Function builds_valid_hashers

Source
pub uninterp fn builds_valid_hashers<T: ?Sized>() -> bool
Expand description

Specifies whether a type conforms to our requirements to be a hash builder in our hash table (and hash set) model.

Our model requires that for any two Hashers that the BuildHasher builds, if they’re both given the same write sequence then their states will match and they’ll produce the same digest when invoked with finish().

The standard library has an axiom that RandomState, the default BuildHasher used by HashMap and HashSet, implements this model. If you want to use some other hash builder type MyHashBuilder, you need to explicitly state your assumption that it does so with assume(vstd::std_specs::hash::builds_valid_hashers::<MyHashBuilder>()).