Specify behavior of std::collections::HashMap

[jaylorch]

This code adds specifications for the standard-library type std::collections::HashMap. It also adds utility structures HashMapWithView and StringHashMap.

Most of the specification for HashMap only applies if you use HashMap<Key, Value>. If you use some custom build hasher, e.g., withHashMap<Key, Value, CustomBuildHasher>, the specification won't specify much.

Likewise, the specification is only meaningful when you know that Key::hash is deterministic and that only identical keys satisfy the executable == operator. We have an axiom that all primitive types and Boxes thereof meet these requirements. But if you want to use some other key type MyKey, you need to explicitly state your assumption that it satisfies these requirements 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 satisfies these requirements so you don't have to make such an assumption.

To make most use of the specification, you should use broadcast use vstd::std_specs::hash::group_hash_axioms;. This will bring various useful axioms about the behavior of a HashMap into the ambient reasoning context. In the future, if we find that having these axioms in scope doesn't impact performance, we may put them into the global ambient context so you don't have to explicitly broadcast use them.

For cases where you want the view of a HashMap to be Map<<Key as View>::V, Value> instead of Map<Key, Value>, use vstd::hash_map::HashMapWithView. For the specific case that you want the key to be String, use vstd::hash_map::StringHashMap.

[jaylorch]

Is verifier::prune_unless_this_module_is_used effective enough that we can just add these axioms into the global ambient context, without worrying about performance implications?