Function obeys_key_model 

pub uninterp spec fn obeys_key_model<Key: ?Sized>() -> bool

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

These requirements are that (1) <Key as PartialEqSpec>::obeys_eq_spec() is true and executable equality is reflexive, symmetric, and transitive; (2) the hash function is deterministic; (3) executable-equal keys have equal hashes; and (4) if Key implements Clone, cloning produces a result structurally identical and executable-equal to its input. Key need not implement Clone. Requirement (2) isn’t satisfied by having Key implement Hash, since this trait doesn’t mandate determinism.

The standard library has axioms that all primitive types, String, str, and Boxes of primitive types 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.