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.

[parno]

Thanks very much for putting this together! It will be very handy to have (even partial) support for reasoning about HashMaps.

[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?

[tjhance]

Sorry for the long delay on this.

We discussed hash map specs for a while at the retreat, and IIRC, the decision then was to add a new trait and add the capability to write specs dependent on this trait bound. However, it might be some time before we get that working.

Meanwhile, this PR is available now, and the feature is a long-requested one. Should we proceed with this, with the expectation of later moving to what we decided on at the retreat?