diff options
| -rw-r--r-- | fstar/Primitives.fst | 28 | ||||
| -rw-r--r-- | tests/hashmap/Hashmap.Properties.fst | 708 |
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. |