Function obeys_key_modelCopy item path

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

The three requirements are (1) the hash function is deterministic, (2) any two keys of type Key are identical if and only if they are considered equal by the executable == operator, and (3) the executable Key::clone function produces a result identical to its input. Requirement (1) isn’t satisfied by having Key implement Hash, since this trait doesn’t mandate determinism.

The standard library has axioms that all primitive types and Boxes thereof obey this model. If you want to use some other key type MyKey, you need to explicitly state your assumption that it does so with assume(vstd::std_specs::hash::obeys_key_model::<MyKey>()). In the future, we plan to devise a way for you to prove that it does so, so that you don’t have to make such an assumption.