summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--fstar/Primitives.fst28
-rw-r--r--tests/hashmap/Hashmap.Properties.fst708
2 files changed, 632 insertions, 104 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index 4642d080..77cf59aa 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -19,7 +19,7 @@ let rec list_update #a ls i x =
(*** Result *)
type result (a : Type0) : Type0 =
-| Return : a -> result a
+| Return : v:a -> result a
| Fail : result a
// Monadic bind and return.
@@ -113,7 +113,7 @@ let scalar_max (ty : scalar_ty) : int =
| U64 -> u64_max
| U128 -> u128_max
-type scalar (ty : scalar_ty) : Type0 = x:int{scalar_min ty <= x && x <= scalar_max ty}
+type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}
let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail
@@ -146,18 +146,18 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
/// The scalar types
-type isize = scalar Isize
-type i8 = scalar I8
-type i16 = scalar I16
-type i32 = scalar I32
-type i64 = scalar I64
-type i128 = scalar I128
-type usize = scalar Usize
-type u8 = scalar U8
-type u16 = scalar U16
-type u32 = scalar U32
-type u64 = scalar U64
-type u128 = scalar U128
+type isize : eqtype = scalar Isize
+type i8 : eqtype = scalar I8
+type i16 : eqtype = scalar I16
+type i32 : eqtype = scalar I32
+type i64 : eqtype = scalar I64
+type i128 : eqtype = scalar I128
+type usize : eqtype = scalar Usize
+type u8 : eqtype = scalar U8
+type u16 : eqtype = scalar U16
+type u32 : eqtype = scalar U32
+type u64 : eqtype = scalar U64
+type u128 : eqtype = scalar U128
/// Negation
let isize_neg = scalar_neg #Isize
diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 14ca7d00..a3e21a16 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -12,6 +12,46 @@ module InteractiveHelpers = FStar.InteractiveHelpers
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+(*** List lemmas *)
+
+val index_append_lem (#a : Type0) (ls0 ls1 : list a) (i : nat{i < length ls0 + length ls1}) :
+ Lemma (
+ (i < length ls0 ==> index (ls0 @ ls1) i == index ls0 i) /\
+ (i >= length ls0 ==> index (ls0 @ ls1) i == index ls1 (i - length ls0)))
+ [SMTPat (index (ls0 @ ls1) i)]
+
+#push-options "--fuel 1"
+let rec index_append_lem #a ls0 ls1 i =
+ match ls0 with
+ | [] -> ()
+ | x :: ls0' ->
+ if i = 0 then ()
+ else index_append_lem ls0' ls1 (i-1)
+#pop-options
+
+// TODO: remove?
+// Returns the index of the value which satisfies the predicate
+val find_index :
+ #a:Type
+ -> f:(a -> Tot bool)
+ -> ls:list a{Some? (find f ls)}
+ -> Tot (i:nat{
+ i < length ls /\
+ begin match find f ls with
+ | None -> False
+ | Some x -> x == index ls i
+ end})
+
+#push-options "--fuel 1"
+let rec find_index #a f ls =
+ match ls with
+ | [] -> assert(False); 0
+ | x :: ls' ->
+ if f x then 0
+ else 1 + find_index f ls'
+#pop-options
+
+
(*** Lemmas about Primitives *)
/// TODO: move those lemmas
@@ -33,6 +73,7 @@ let rec list_update_index_dif_lem #a ls i x j =
(*** Utilities *)
+// TODO: filter the utilities
val find_update:
#a:Type
@@ -60,6 +101,16 @@ let rec for_allP (f : 'a -> Tot Type0) (l : list 'a) : Tot Type0 =
| [] -> True
| hd::tl -> f hd /\ for_allP f tl
+val for_all_i_aux: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> nat -> Tot bool
+let rec for_all_i_aux (f : nat -> 'a -> Tot bool) (l : list 'a) (i : nat) : Tot bool =
+ match l with
+ | [] -> true
+ | hd::tl -> f i hd && for_all_i_aux f tl (i+1)
+
+val for_all_i: #a:Type -> f:(nat -> a -> Tot bool) -> list a -> Tot bool
+let for_all_i (f : nat -> 'a -> Tot bool) (l : list 'a) : Tot bool =
+ for_all_i_aux f l 0
+
val pairwise_relP : #a:Type -> pred:(a -> a -> Tot Type0) -> ls:list a -> Tot Type0
let rec pairwise_relP #a pred ls =
match ls with
@@ -94,13 +145,16 @@ let fst_is_disctinct (#a : eqtype) (#b : Type0) (p0 : a & b) (p1 : a & b) : Type
(*** Invariants, models *)
+(*
/// "Natural" length function for [list_t]
/// TODO: remove? we can reason simply with [list_t_v]
let rec list_t_len (#t : Type0) (ls : list_t t) : nat =
match ls with
| ListNil -> 0
| ListCons _ _ tl -> 1 + list_t_len tl
+*)
+(*
/// "Natural" append function for [list_t]
/// TODO: remove? we can reason simply with [list_t_v]
#push-options "--fuel 1"
@@ -110,9 +164,12 @@ let rec list_t_append (#t : Type0) (ls0 ls1 : list_t t) :
| ListNil -> ls1
| ListCons x v tl -> ListCons x v (list_t_append tl ls1)
#pop-options
+*)
/// The "key" type
-type key = usize
+type key : eqtype = usize
+
+type hash : eqtype = usize
type binding (t : Type0) = key & t
@@ -127,6 +184,10 @@ let rec list_t_v (#t : Type0) (ls : list_t t) : assoc_list t =
| ListNil -> []
| ListCons k v tl -> (k,v) :: list_t_v tl
+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.
/// Rk.: I hesitated to use [concatMap]
let slots_t_v (#t : Type0) (slots : slots_t t) : assoc_list t =
@@ -136,7 +197,21 @@ let slots_t_v (#t : Type0) (slots : slots_t t) : assoc_list t =
let hash_map_t_v (#t : Type0) (hm : hash_map_t t) : assoc_list t =
slots_t_v hm.hash_map_slots
+let hash_key (k : key) : hash =
+ Return?.v (hash_key_fwd k)
+
+let hash_mod_key (k : key) (len : usize{len > 0}) : hash =
+ (hash_key k) % len
+
let same_key (#t : Type0) (k : key) (b : binding t) : bool = fst b = k
+
+// We take a [nat] instead of a [hash] on purpose
+let same_hash_mod_key (#t : Type0) (len : usize{len > 0}) (h : nat) (b : binding t) : bool =
+ hash_mod_key (fst b) len = h
+
+// We take a [nat] instead of a [hash] on purpose
+(*let same_hash (#t : Type0) (h : nat) (b : binding t) : bool = hash_key (fst b) = h *)
+
let binding_neq (#t : Type0) (b0 b1 : binding t) : bool = fst b0 <> fst b1
let has_same_binding (#t : Type0) (al : assoc_list t) ((k,v) : binding t) : Type0 =
@@ -147,10 +222,32 @@ let has_same_binding (#t : Type0) (al : assoc_list t) ((k,v) : binding t) : Type
let hash_map_t_mem (#t : Type0) (hm : hash_map_t t) (k : key) : bool =
existsb (same_key k) (hash_map_t_v hm)
-let hash_map_t_find (#t : Type0) (hm : hash_map_t t) (k : key) : option t =
+let hash_map_t_len (#t : Type0) (hm : hash_map_t t) : nat =
+ hm.hash_map_num_entries
+
+let slot_t_v_find (#t : Type0) (k : key) (slot : list (binding t)) : option t =
+ match find (same_key k) slot with
+ | None -> None
+ | Some (_, v) -> Some v
+
+let slot_t_find (#t : Type0) (k : key) (slot : list_t t) : option t =
+ match find (same_key k) (list_t_v slot) with
+ | None -> None
+ | Some (_, v) -> Some v
+
+// This is a simpler version of the "find" function, which captures the essence
+// of what happens.
+let hash_map_t_find
+ (#t : Type0) (hm : hash_map_t t{length hm.hash_map_slots > 0}) (k : key) : option t =
+ let slots = hm.hash_map_slots in
+ let i = hash_mod_key k (length slots) in
+ let slot = index slots i in
+ slot_t_find k slot
+
+(*let hash_map_t_find (#t : Type0) (hm : hash_map_t t) (k : key) : option t =
match find (same_key k) (hash_map_t_v hm) with
| None -> None
- | Some (_, v) -> Some v
+ | Some (_, v) -> Some v*)
/// Auxiliary function stating that two associative lists are "equivalent"
let assoc_list_equiv (#t : Type0) (al0 al1 : assoc_list t) : Type0 =
@@ -159,15 +256,130 @@ let assoc_list_equiv (#t : Type0) (al0 al1 : assoc_list t) : Type0 =
// And the reverse is true
for_allP (has_same_binding al0) al1
-/// Base invariant for the hashmap (might temporarily be broken at some point)
+// Introducing auxiliary definitions to help deal with the quantifiers
+
+let not_same_keys_at_j_k
+ (#t : Type0) (ls : list_t t) (j:nat{j < list_t_len ls}) (k:nat{k < list_t_len ls}) :
+ Type0 =
+ fst (list_t_index ls j) <> fst (list_t_index ls k)
+
+(*let not_same_keys_at_j_k
+ (#t : Type0) (ls : list_t t) (j:nat{j < list_t_len ls}) (k:nat{k < list_t_len ls}) :
+ Type0 =
+ fst (list_t_index ls j) <> fst (list_t_index ls k)*)
+
+type slot_t_inv_hash_key_f (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) =
+ (j:nat{j < list_t_len slot}) ->
+ Lemma (hash_mod_key (fst (list_t_index slot j)) len = i)
+ [SMTPat (hash_mod_key (fst (list_t_index slot j)) len)]
+
+type slot_t_inv_not_same_keys_f (#t : Type0) (i : usize) (slot : list_t t) =
+ (j:nat{j < list_t_len slot})
+ -> (k:nat{k < list_t_len slot /\ j < k})
+ -> Lemma (not_same_keys_at_j_k slot j k)
+ [SMTPat (not_same_keys_at_j_k slot j k)]
+
+(**)
+
+/// Invariants for the slots
+/// Rk.: making sure the quantifiers instantiations work was painful. As always.
+
+let slot_t_v_inv
+(#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list (binding t)) : bool =
+ // All the bindings are in the proper slot
+ for_all (same_hash_mod_key len i) slot &&
+ // All the keys are pairwise distinct
+ pairwise_rel binding_neq slot
+
+let slot_t_inv (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) : bool =
+ // All the bindings are in the proper slot
+ for_all (same_hash_mod_key len i) (list_t_v slot) &&
+ // All the keys are pairwise distinct
+ pairwise_rel binding_neq (list_t_v slot)
+
+(*
+/// Invariants for the slots
+/// Rk.: making sure the quantifiers instantiations work was painful. As always.
+let slot_t_inv (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t) : Type0 =
+ // All the hashes of the keys are equal to the current hash
+ (forall (j:nat{j < list_t_len slot}).
+ {:pattern (list_t_index slot j)}
+ hash_mod_key (fst (list_t_index slot j)) len = i) /\
+ // All the keys are pairwise distinct
+ (forall (j:nat{j < list_t_len slot}) (k:nat{k < list_t_len slot /\ j < k}).
+ {:pattern not_same_keys_at_j_k slot j k}
+ k <> j ==> not_same_keys_at_j_k slot j k)
+
+/// Helpers to deal with the quantifier proofs
+let slot_t_inv_to_funs
+ (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t{slot_t_inv len i slot}) :
+ slot_t_inv_hash_key_f len i slot & slot_t_inv_not_same_keys_f i slot =
+ let f : slot_t_inv_hash_key_f len i slot =
+ fun j -> ()
+ in
+ let g : slot_t_inv_not_same_keys_f i slot =
+ fun j k -> ()
+ in
+ (f, g)
+
+let slot_t_inv_from_funs_lem
+ (#t : Type0) (len : usize{len > 0}) (i : usize) (slot : list_t t)
+ (f : slot_t_inv_hash_key_f len i slot)
+ (g : slot_t_inv_not_same_keys_f i slot) :
+ Lemma (slot_t_inv len i slot) =
+ // Dealing with quantifiers is annoying, like always
+ let f' (j:nat{j < list_t_len slot}) :
+ Lemma (hash_mod_key (fst (list_t_index slot j)) len = i)
+ [SMTPat (hash_mod_key (fst (list_t_index slot j)) len)]
+ =
+ f j
+ in
+ let g' (j:nat{j < list_t_len slot}) (k:nat{k < list_t_len slot /\ j < k}) :
+ Lemma (not_same_keys_at_j_k slot j k)
+ [SMTPat (not_same_keys_at_j_k slot j k)]
+ =
+ g j k
+ in
+ ()
+*)
+
+let slots_t_inv (#t : Type0) (slots : slots_t t{length slots <= usize_max}) : Type0 =
+ forall(i:nat{i < length slots}).
+ {:pattern index slots i}
+ slot_t_inv (length slots) i (index slots i)
+
+type slots_t_inv_f (#t : Type0) (slots : slots_t t{length slots <= usize_max}) =
+ (i:nat{i < length slots}) ->
+ Lemma (slot_t_inv (length slots) i (index slots i))
+
+let slots_t_inv_to_fun
+ (#t : Type0) (slots : slots_t t{length slots <= usize_max /\ slots_t_inv slots}) :
+ slots_t_inv_f slots =
+ fun i -> ()
+
+let slots_t_from_fun
+ (#t : Type0) (slots : slots_t t{length slots <= usize_max})
+ (f : slots_t_inv_f slots) :
+ Lemma (slots_t_inv slots) =
+ let f' (i:nat{i < length slots}) :
+ Lemma (slot_t_inv (length slots) i (index slots i))
+ [SMTPat (slot_t_inv (length slots) i (index slots i))]
+ =
+ f i
+ in
+ ()
+
+/// Base invariant for the hashmap (the complete invariant can be temporarily
+/// broken between the moment we inserted an element and the moment we resize)
let hash_map_t_base_inv (#t : Type0) (hm : hash_map_t t) : Type0 =
let al = hash_map_t_v hm in
// [num_entries] correctly tracks the number of entries in the table
+ // Note that it gives us that the length of the slots array is <= usize_max
hm.hash_map_num_entries = length al /\
- // All the keys are pairwise distinct
- pairwise_rel binding_neq al /\
- // The capacity must be > 0 (otherwise we can't resize, because we multiply
- // the capacity by two!)
+ // Slots invariant
+ slots_t_inv hm.hash_map_slots /\
+ // The capacity must be > 0 (otherwise we can't resize, because we
+ // multiply the capacity by two!)
length hm.hash_map_slots > 0 /\
// Load computation
begin
@@ -192,58 +404,84 @@ let hash_map_t_is_al (#t : Type0) (hm : hash_map_t t) (al : assoc_list t) : Type
let hm_al = hash_map_t_v hm in
assoc_list_equiv hm_al al
+(*
/// The invariant we reveal to the user
let hash_map_t_inv_repr (#t : Type0) (hm : hash_map_t t) (al : assoc_list t) : Type0 =
// The hash map invariant is satisfied
hash_map_t_inv hm /\
// And it can be seen as the given associative list
hash_map_t_is_al hm al
-
-let hash_map_len (#t : Type0) (hm : hash_map_t t) : nat =
- hm.hash_map_num_entries
+*)
(*** Proofs *)
(**** allocate_slots *)
+
+/// Auxiliary lemma
+val slots_t_all_nil_inv_lem
+ (#t : Type0) (slots : vec (list_t t){length slots <= usize_max}) :
+ Lemma (requires (forall (i:nat{i < length slots}). index slots i == ListNil))
+ (ensures (slots_t_inv slots))
+
+#push-options "--fuel 1"
+let slots_t_all_nil_inv_lem #t slots = ()
+#pop-options
+
+val slots_t_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 == []))
+
+#push-options "--fuel 1"
+let rec slots_t_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);
+ assert(index slots 0 == ListNil)
+#pop-options
+
+/// [allocate_slots]
val hash_map_allocate_slots_fwd_lem
(t : Type0) (slots : vec (list_t t)) (n : usize) :
Lemma
- (requires (slots_t_v slots == [] /\ length slots + n <= usize_max))
+ (requires (length slots + n <= usize_max))
(ensures (
match hash_map_allocate_slots_fwd t slots n with
| Fail -> False
| Return slots' ->
- slots_t_v slots' == [] /\
- length slots' = length slots + n))
+ length slots' = length slots + n /\
+ // We leave the already allocated slots unchanged
+ (forall (i:nat{i < length slots}). index slots' i == index slots i) /\
+ // We allocate n additional empty slots
+ (forall (i:nat{length slots <= i /\ i < length slots'}). index slots' i == ListNil)))
(decreases (hash_map_allocate_slots_decreases t slots n))
#push-options "--fuel 1"
let rec hash_map_allocate_slots_fwd_lem t slots n =
- if n = 0 then ()
- else
+ begin match n with
+ | 0 -> ()
+ | _ ->
begin match vec_push_back (list_t t) slots ListNil with
- | Fail -> assert(False)
- | Return v ->
- (* Prove that the new slots [v] represent an empty mapping *)
- assert(v == slots @ [ListNil]);
- map_append list_t_v slots [ListNil];
- assert(map list_t_v v == map list_t_v slots @ map list_t_v [ListNil]);
- assert_norm(map (list_t_v #t) [ListNil] == [[]]);
- flatten_append (map list_t_v slots) [[]];
- assert(slots_t_v v == slots_t_v slots @ slots_t_v [ListNil]);
- assert_norm(slots_t_v #t [ListNil] == []);
- assert(slots_t_v v == slots_t_v slots @ []);
- assert(slots_t_v v == slots_t_v slots);
- assert(slots_t_v v == []);
+ | Fail -> ()
+ | Return slots1 ->
begin match usize_sub n 1 with
- | Fail -> assert(False)
+ | Fail -> ()
| Return i ->
- hash_map_allocate_slots_fwd_lem t v i;
- begin match hash_map_allocate_slots_fwd t v i with
- | Fail -> assert(False)
- | Return v0 -> ()
+ hash_map_allocate_slots_fwd_lem t slots1 i;
+ begin match hash_map_allocate_slots_fwd t slots1 i with
+ | Fail -> ()
+ | Return slots2 ->
+ assert(length slots1 = length slots + 1);
+ assert(slots1 == slots @ [ListNil]); // Triggers patterns
+ assert(index slots1 (length slots) == index [ListNil] 0); // Triggers patterns
+ assert(index slots1 (length slots) == ListNil)
end
end
end
+ end
#pop-options
(**** new_with_capacity *)
@@ -260,9 +498,18 @@ val hash_map_new_with_capacity_fwd_lem
(ensures (
match hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor with
| Fail -> False
- | Return hm -> hash_map_t_inv_repr hm []))
-
-#push-options "--fuel 1"
+ | Return hm ->
+ // The hash map has the specified capacity - we need to reveal this
+ // otherwise the pre of [hash_map_t_find] is not satisfied.
+ length hm.hash_map_slots = capacity /\
+ // The hash map has 0 values
+ hash_map_t_len hm = 0 /\
+ // It contains no bindings
+ (forall k. hash_map_t_find hm k == None) /\
+ // We need this low-level property for the invariant
+ (forall(i:nat{i < length hm.hash_map_slots}). index hm.hash_map_slots i == ListNil)))
+
+#push-options "--z3rlimit 50 --fuel 1"
let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize)
(max_load_dividend : usize) (max_load_divisor : usize) =
let v = vec_new (list_t t) in
@@ -278,26 +525,35 @@ let hash_map_new_with_capacity_fwd_lem (t : Type0) (capacity : usize)
| Fail -> assert(False)
| Return i0 ->
let hm = Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0 in
- // The base invariant
- let al = hash_map_t_v hm in
- assert(hash_map_t_base_inv hm);
- assert(hash_map_t_inv hm);
- assert(hash_map_t_is_al hm [])
+ slots_t_all_nil_inv_lem v0
end
end
end
#pop-options
(**** new *)
-/// [new] doesn't fail and returns an empty hash map.
-val hash_map_new_fwd_lem (t : Type0) :
+/// [new] doesn't fail and returns an empty hash map
+val hash_map_new_fwd_lem_fun (t : Type0) :
Lemma
(ensures (
match hash_map_new_fwd t with
| Fail -> False
- | Return hm -> hash_map_t_inv_repr hm []))
+ | Return hm ->
+ // The hash map invariant is satisfied
+ hash_map_t_inv hm /\
+ // The hash map has 0 values
+ hash_map_t_len hm = 0 /\
+ // It contains no bindings
+ (forall k. hash_map_t_find hm k == None)))
-let hash_map_new_fwd_lem t = hash_map_new_with_capacity_fwd_lem t 32 4 5
+#push-options "--fuel 1"
+let hash_map_new_fwd_lem_fun t =
+ hash_map_new_with_capacity_fwd_lem t 32 4 5;
+ 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
+#pop-options
(**** clear_slots *)
/// [clear_slots] doesn't fail and simply clears the slots starting at index i
@@ -340,34 +596,9 @@ let rec hash_map_clear_slots_fwd_back_lem
else ()
#pop-options
-/// Auxiliary lemma:
-/// if all the slots in a vector are [ListNil], then this vector viewed as a list
-/// is empty.
-#push-options "--fuel 1"
-let rec slots_t_v_all_nil_is_empty_lem (#t : Type0) (slots : slots_t t) :
- Lemma (requires (forall (i:nat{i < length slots}). index slots i == ListNil))
- (ensures (slots_t_v slots == []))
- =
- match slots with
- | [] -> ()
- | s :: slots' ->
- (* The following assert helps the instantiation of quantifiers... *)
- assert(forall (i:nat{i < length slots'}). index slots' i == index slots (i+1));
- slots_t_v_all_nil_is_empty_lem slots';
- assert(slots_t_v slots == flatten (map list_t_v (s :: slots')));
- assert(slots_t_v slots == flatten (list_t_v s :: map list_t_v slots'));
- assert(slots_t_v slots == append (list_t_v s) (flatten (map list_t_v slots')));
- assert(slots_t_v slots == append (list_t_v s) (flatten (map list_t_v slots')));
- assert(slots_t_v slots == append (list_t_v s) []);
- assert(slots_t_v slots == (list_t_v s) @ []); // Triggers an SMT pat
- assert(slots_t_v slots == list_t_v s);
- assert(index slots 0 == s);
- assert(slots_t_v slots == [])
-#pop-options
-
(**** clear *)
/// [clear] doesn't fail and turns the hash map into an empty map
-val hash_map_clear_fwd_back_lem
+val hash_map_clear_fwd_back_lem_fun
(t : Type0) (self : hash_map_t t) :
Lemma
(requires (hash_map_t_inv self))
@@ -375,11 +606,16 @@ val hash_map_clear_fwd_back_lem
match hash_map_clear_fwd_back t self with
| Fail -> False
| Return hm ->
- hash_map_t_inv_repr hm []))
+ // The hash map invariant is satisfied
+ hash_map_t_inv hm /\
+ // The hash map has 0 values
+ hash_map_t_len hm = 0 /\
+ // It contains no bindings
+ (forall k. hash_map_t_find hm k == None)))
// Being lazy: fuel 1 helps a lot...
#push-options "--fuel 1"
-let hash_map_clear_fwd_back_lem t self =
+let hash_map_clear_fwd_back_lem_fun t self =
let p = self.hash_map_max_load_factor in
let i = self.hash_map_max_load in
let v = self.hash_map_slots in
@@ -391,12 +627,10 @@ let hash_map_clear_fwd_back_lem t self =
let hm1 = Mkhash_map_t 0 p i slots1 in
assert(hash_map_t_base_inv hm1);
assert(hash_map_t_inv hm1);
- assert(hash_map_t_is_al hm1 []);
- assert(hash_map_t_inv_repr hm1 [])
+ assert(hash_map_t_is_al hm1 [])
end
#pop-options
-
(**** len *)
/// [len]: we link it to a non-failing function.
@@ -406,14 +640,14 @@ val hash_map_len_fwd_lem (t : Type0) (self : hash_map_t t) :
Lemma (
match hash_map_len_fwd t self with
| Fail -> False
- | Return l -> l = hash_map_len self)
+ | Return l -> l = hash_map_t_len self)
let hash_map_len_fwd_lem t self = ()
(**** insert_in_list *)
-/// [insert_in_list_fwd]: returns true iff the key is not in the list
+/// [insert_in_list_fwd]: returns true iff the key is not in the list (functional version)
val hash_map_insert_in_list_fwd_lem
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Lemma
@@ -421,7 +655,7 @@ val hash_map_insert_in_list_fwd_lem
match hash_map_insert_in_list_fwd t key value ls with
| Fail -> False
| Return b ->
- b <==> (find (same_key key) (list_t_v ls) == None)))
+ b <==> (slot_t_find key ls == None)))
(decreases (hash_map_insert_in_list_decreases t key value ls))
#push-options "--fuel 1"
@@ -444,11 +678,227 @@ let rec hash_map_insert_in_list_fwd_lem t key value ls =
end
#pop-options
+(*
+/// [insert_in_list]
+// TODO: remove
+val hash_map_insert_in_list_back_lem
+ (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list_t t) :
+ Lemma
+ (requires (slot_t_inv len (hash_mod_key key len) ls))
+ (ensures (
+ match hash_map_insert_in_list_back t key value ls with
+ | Fail -> False
+ | Return ls' ->
+ // The invariant is preserved
+ slot_t_inv len (hash_mod_key key len) ls' /\
+ // [key] maps to [value]
+ slot_t_find key ls' == Some value /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> slot_t_find k' ls' == slot_t_find k' ls) /\
+ // The length is incremented, iff we inserted a new key
+ (match slot_t_find key ls with
+ | None ->
+ list_t_v ls' == list_t_v ls @ [(key,value)] /\
+ list_t_len ls' = list_t_len ls + 1
+ | Some _ ->
+ list_t_v ls' == find_update (same_key key) (list_t_v ls) (key,value) /\
+ list_t_len ls' = list_t_len ls)))
+ (decreases (hash_map_insert_in_list_decreases t key value ls))
+
+// I suffered a bit below, but as usual, for the wrong reasons: quantifiers in F*
+// are really too painful to work with...
+#push-options "--z3rlimit 200 --fuel 1"
+let rec hash_map_insert_in_list_back_lem t len key value ls =
+ let h = hash_mod_key key len in
+ begin match ls with
+ | ListCons ckey cvalue ls0 ->
+ let b = ckey = key in
+ if b
+ then
+ begin
+ let ls1 = ListCons ckey value ls0 in
+ let ls_hash_key_lem, ls_not_same_keys_lem = slot_t_inv_to_funs len h ls in
+ let ls1_hash_key_lem : slot_t_inv_hash_key_f len h ls1 =
+ fun j -> if j = 0 then () else ls_hash_key_lem j
+ in
+ let ls1_not_same_keys_lem : slot_t_inv_not_same_keys_f h ls1 =
+ fun j k -> ls_not_same_keys_lem j k
+ in
+ slot_t_inv_from_funs_lem len h ls1 ls1_hash_key_lem ls1_not_same_keys_lem;
+ assert(slot_t_inv len (hash_mod_key key len) ls1)
+ end
+ else
+ begin
+ let ls_hash_key_lem, ls_not_same_keys_lem = slot_t_inv_to_funs len h ls in
+ let ls0_hash_key_lem : slot_t_inv_hash_key_f len h ls0 =
+ fun j -> ls_hash_key_lem (j + 1)
+ in
+ let ls0_not_same_keys_lem : slot_t_inv_not_same_keys_f h ls0 =
+ fun j k -> ls_not_same_keys_lem (j + 1) (k + 1)
+ in
+ slot_t_inv_from_funs_lem len h ls0 ls0_hash_key_lem ls0_not_same_keys_lem;
+ assert(slot_t_inv len (hash_mod_key key len) ls0);
+ hash_map_insert_in_list_back_lem t len key value ls0;
+ match hash_map_insert_in_list_back t key value ls0 with
+ | Fail -> ()
+ | Return l ->
+ let ls1 = ListCons ckey cvalue l in
+ let l_hash_key_lem, l_not_same_keys_lem = slot_t_inv_to_funs len h l in
+ let ls1_hash_key_lem : slot_t_inv_hash_key_f len h ls1 =
+ fun j ->
+ if j = 0 then
+ begin
+ ls_hash_key_lem 0;
+ assert(hash_mod_key (fst (list_t_index ls1 j)) len = h)
+ end
+ else l_hash_key_lem (j - 1)
+ in
+ (* Disjunction on whether we added an element or not *)
+ begin match slot_t_find key ls0 with
+ | None ->
+ (* We added an element *)
+ assert(list_t_v l == list_t_v ls0 @ [(key,value)]);
+ // assert(list_t_v ls1 == list_t_v ls @ [(key,value)]);
+ let ls1_not_same_keys_lem : slot_t_inv_not_same_keys_f h ls1 =
+ fun j k ->
+ if 0 < j then
+ l_not_same_keys_lem (j-1) (k-1)
+ else //if k < list_t_len ls then
+ begin
+// assert_norm(length [(key,value)] = 1);
+ assert(list_t_index ls1 j == (ckey, cvalue));
+ assert(list_t_v ls1 == (ckey, cvalue) :: list_t_v l);
+ assert(list_t_index ls1 k == list_t_index l (k-1));
+// index_append_lem (list_t_v ls0) [(key,value)] (j-1);
+ index_append_lem (list_t_v ls0) [(key,value)] (k-1);
+ if k < list_t_len l then
+ begin
+ assert(list_t_index ls1 k == list_t_index ls0 (k-1));
+ admit()
+ end
+ else
+ admit()
+ end
+ in
+ slot_t_inv_from_funs_lem len h ls1 ls1_hash_key_lem ls1_not_same_keys_lem
+ | _ ->
+ (* We simply updated a binding *)
+ admit()
+ end
+ end
+ | ListNil ->
+ let ls0 = ListCons key value ListNil in
+ assert_norm(list_t_len ls0 == 1);
+ let ls0_hash_key_lem : slot_t_inv_hash_key_f len h ls0 =
+ fun j -> ()
+ in
+ let ls0_not_same_keys_lem : slot_t_inv_not_same_keys_f h ls0 =
+ fun j k -> ()
+ in
+ slot_t_inv_from_funs_lem len h ls0 ls0_hash_key_lem ls0_not_same_keys_lem
+ end
+#pop-options
+*)
+
+(**** insert_no_resize *)
+
+(*val hash_map_insert_no_resize_fwd_back_lem
+ (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
+ Lemma (requires (hash_map_t_inv self))
+ (ensures (
+ match hash_map_insert_no_resize_fwd_back t self key value with
+ | Fail ->
+ (* If we fail, it is necessarily because:
+ * - we tried to add a new *key* (there was no binding for the key)
+ * - the [num_entries] counter is already saturaed *)
+ hash_map_t_find self key == None /\
+ hash_map_t_len self = usize_max
+ | Return hm ->
+ // The invariant is preserved
+ hash_map_t_inv hm /\
+ // [key] maps to [value]
+ hash_map_t_find hm key == Some value /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> hash_map_t_find hm k' == hash_map_t_find self k') /\
+ // The length is incremented, iff we inserted a new key
+ (match hash_map_t_find self key with
+ | None -> hash_map_t_len hm = hash_map_t_len hm + 1
+ | Some _ -> hash_map_t_len hm = hash_map_t_len hm)))
+
+let hash_map_insert_no_resize_fwd_back_lem 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 ->
+ begin
+ hash_map_insert_in_list_fwd_lem t key value l;
+ match hash_map_insert_in_list_fwd t key value l with
+ | Fail -> ()
+ | Return b ->
+ if b
+ then
+ begin match usize_add i0 1 with
+ | Fail ->
+ assert(slot_t_find key l == None);
+ assert(hash_map_t_len self = usize_max);
+ ()
+ | Return i3 ->
+ assert(l == index v hash_mod);
+ slots_t_inv_to_fun v hash_mod;
+ assert(slot_t_inv hash_mod (index v hash_mod));
+ assert(slot_t_inv (hash_key key) l);
+ hash_map_insert_in_list_back_lem t key value l;
+ begin match hash_map_insert_in_list_back t key value l with
+ | Fail -> admit()
+ | Return l0 ->
+ begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+ | Fail -> admit()
+ | Return v0 ->
+ let self0 = Mkhash_map_t i3 p i1 v0 in admit() //Return self0
+ end
+ end
+ end
+ else
+ begin match hash_map_insert_in_list_back t key value l with
+ | Fail -> admit()
+ | Return l0 ->
+ begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+ | Fail -> admit()
+ | Return v0 ->
+ let self0 = Mkhash_map_t i0 p i1 v0 in admit() //Return self0
+ end
+ end
+ end
+ end
+ end
+ end*)
+
/// The proofs about [insert_in_list] backward are easier to do in several steps:
/// extrinsic proofs to the rescue!
-
-/// [insert_in_list]: if the key is not in the map, appends a new bindings
-val hash_map_insert_in_list_back_lem_append
+/// Rk.: those proofs actually caused a lot of trouble because:
+/// - F* is extremely bad at reasoning with quantifiers, which is made worse by
+/// the fact we are blind when making proofs. This forced us to be extremely
+/// careful about the way we wrote our specs/invariants (by writing "functional"
+/// specs and invariants, mostly, so as not to manipulate quantifiers)
+/// - we can't easily prove intermediate results which require a recursive proofs
+/// inside of other proofs, meaning that whenever we need such a result we need
+/// to write an intermediate lemma, which is extremely cumbersome.
+/// Note that in a theorem prover with tactics, most of the below proof would have
+/// been extremely straightforward. In particular, we wouldn't have needed to think
+/// much about the invariants, nor to cut the proofs into very small, modular lemmas.
+
+/// [insert_in_list]: if the key is not in the map, appends a new bindings (functional version)
+val hash_map_insert_in_list_back_lem_append_fun
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Lemma
(requires (
@@ -461,15 +911,15 @@ val hash_map_insert_in_list_back_lem_append
(decreases (hash_map_insert_in_list_decreases t key value ls))
#push-options "--fuel 1"
-let rec hash_map_insert_in_list_back_lem_append t key value ls =
+let rec hash_map_insert_in_list_back_lem_append_fun t key value ls =
begin match ls with
| ListCons ckey cvalue ls0 ->
let b = ckey = key in
if b
- then () //let ls1 = ListCons ckey value ls0 in Return ls1
+ then ()
else
begin
- hash_map_insert_in_list_back_lem_append t key value ls0;
+ hash_map_insert_in_list_back_lem_append_fun t key value ls0;
match hash_map_insert_in_list_back t key value ls0 with
| Fail -> ()
| Return l -> ()
@@ -478,8 +928,8 @@ let rec hash_map_insert_in_list_back_lem_append t key value ls =
end
#pop-options
-/// [insert_in_list]: if the key is in the map, we update the binding
-val hash_map_insert_in_list_back_lem_update
+/// [insert_in_list]: if the key is in the map, we update the binding (functional version)
+val hash_map_insert_in_list_back_lem_update_fun
(t : Type0) (key : usize) (value : t) (ls : list_t t) :
Lemma
(requires (
@@ -492,7 +942,7 @@ val hash_map_insert_in_list_back_lem_update
(decreases (hash_map_insert_in_list_decreases t key value ls))
#push-options "--fuel 1"
-let rec hash_map_insert_in_list_back_lem_update t key value ls =
+let rec hash_map_insert_in_list_back_lem_update_fun t key value ls =
begin match ls with
| ListCons ckey cvalue ls0 ->
let b = ckey = key in
@@ -500,7 +950,7 @@ let rec hash_map_insert_in_list_back_lem_update t key value ls =
then ()
else
begin
- hash_map_insert_in_list_back_lem_update t key value ls0;
+ hash_map_insert_in_list_back_lem_update_fun t key value ls0;
match hash_map_insert_in_list_back t key value ls0 with
| Fail -> ()
| Return l -> ()
@@ -509,6 +959,84 @@ let rec hash_map_insert_in_list_back_lem_update t key value ls =
end
#pop-options
+/// Auxiliary lemmas
+/// Reasoning about the result of [insert_in_list], converted to a "regular" list.
+/// Note that in F* we can't have recursive proofs inside of other proofs, contrary
+/// to Coq, which makes it a bit cumbersome to prove auxiliary results like the
+/// following ones...
+
+val slot_t_v_for_all_binding_neq_append_lem
+ (t : Type0) (key : usize) (value : t) (ls : list (binding t)) (b : binding t) :
+ Lemma
+ (requires (
+ fst b <> key /\
+ for_all (binding_neq b) ls /\
+ slot_t_v_find key ls == None))
+ (ensures (
+ for_all (binding_neq b) (ls @ [(key,value)])))
+
+#push-options "--fuel 1"
+let rec slot_t_v_for_all_binding_neq_append_lem t key value ls b =
+ match ls with
+ | [] -> ()
+ | (ck, cv) :: cls ->
+ slot_t_v_for_all_binding_neq_append_lem t key value cls b
+#pop-options
+
+val slot_t_v_inv_not_find_append_end_inv_lem
+ (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list (binding t)) :
+ Lemma
+ (requires (
+ slot_t_v_inv len (hash_mod_key key len) ls /\
+ slot_t_v_find key ls == None))
+ (ensures (
+ let ls' = ls @ [(key,value)] in
+ slot_t_v_inv len (hash_mod_key key len) ls' /\
+ (slot_t_v_find key ls' == Some value) /\
+ (forall k'. k' <> key ==> slot_t_v_find k' ls' == slot_t_v_find k' ls)))
+
+#push-options "--fuel 1"
+let rec slot_t_v_inv_not_find_append_end_inv_lem t len key value ls =
+ match ls with
+ | [] -> ()
+ | (ck, cv) :: cls ->
+ slot_t_v_inv_not_find_append_end_inv_lem t len key value cls;
+ let h = hash_mod_key key len in
+ let ls' = ls @ [(key,value)] in
+ assert(for_all (same_hash_mod_key len h) ls');
+ slot_t_v_for_all_binding_neq_append_lem t key value cls (ck, cv);
+ assert(pairwise_rel binding_neq ls');
+ assert(slot_t_v_inv len h ls')
+#pop-options
+
+/// [insert_in_list]: if the key is not in the map, appends a new bindings (quantifiers)
+val hash_map_insert_in_list_back_lem_append
+ (t : Type0) (len : usize{len > 0}) (key : usize) (value : t) (ls : list_t t) :
+ Lemma
+ (requires (
+ slot_t_inv len (hash_mod_key key len) ls /\
+ find (same_key key) (list_t_v ls) == None))
+ (ensures (
+ match hash_map_insert_in_list_back t key value ls with
+ | Fail -> False
+ | Return ls' ->
+ list_t_v ls' == list_t_v ls @ [(key,value)] /\
+ // The invariant is preserved
+ slot_t_inv len (hash_mod_key key len) ls' /\
+ // [key] maps to [value]
+ slot_t_find key ls' == Some value /\
+ // The other bindings are preserved
+ (forall k'. k' <> key ==> slot_t_find k' ls' == slot_t_find k' ls)))
+
+let hash_map_insert_in_list_back_lem_append t len key value ls =
+ hash_map_insert_in_list_back_lem_append_fun t key value ls;
+ match hash_map_insert_in_list_back t key value ls with
+ | Fail -> ()
+ | Return ls' ->
+ assert(list_t_v ls' == list_t_v ls @ [(key,value)]);
+ slot_t_v_inv_not_find_append_end_inv_lem t len key value (list_t_v ls)
+
+(*
(**** insert_no_resize *)
/// Same as for [insert_in_list]: we do the proofs in several, modular steps.