Expand description
This code adds specifications for the standard-library types
std::collections::HashMap and std::collections::HashSet.
Most of the specification only applies if you use HashMap<Key, Value> or HashSet<Key>. 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 the Key
obeys our hash table model, i.e., (1) Key::hash is
deterministic, (2) any two Keys are identical if and only if the
executable == operator considers them equal, and (3)
Key::clone produces a result equal to its input. We have an
axiom that all primitive types and Boxes thereof obey this
model. But 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.
By default, the Verus standard library brings useful axioms
about the behavior of HashMap and HashSet into the ambient
reasoning context by broadcasting the group
vstd::std_specs::hash::group_hash_axioms.
Structs§
- ExDefault
Hasher - Specifications for the behavior of
std::collections::hash_map::DefaultHasher. - ExHash
Map - Specifications for the behavior of
std::collections::HashMap. - ExHash
Set - Specifications for the behavior of
std::collections::HashSet. - ExKeys
- Specifications for the behavior of
std::collections::hash_map::Keys. - ExMap
Iter - ExRandom
State - Specifications for the behavior of
std::hash::RandomState. - ExSet
Iter - ExValues
- Specifications for the behavior of
std::collections::hash_map::Values. - Keys
Ghost Iterator - MapIter
Ghost Iterator - SetIter
Ghost Iterator - Values
Ghost Iterator
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 380_ Default Hasher_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 381_ Default Hasher_ 32__ 58__ 58__ 32_ write - _verus_
external_ ⚠fn_ specification_ 382_ Default Hasher_ 32__ 58__ 58__ 32_ finish - _verus_
external_ ⚠fn_ specification_ 383_ Keys_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 384_ Values_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 385_ hash__ map_ 32__ 58__ 58__ 32_ Iter_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 386_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 387_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 388_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 389__ 60__ 32_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ K_ 44__ 32_ V_ 44__ 32_ S_ 32__ 62__ 32_ as_ 32_ Clone_ 32__ 62__ 32__ 58__ 58__ 32_ clone - _verus_
external_ ⚠fn_ specification_ 390_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 391__ 60__ 32_ Hash Map_ 32__ 60__ 32_ K_ 44__ 32_ V_ 44__ 32_ S_ 44__ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ default_ 32__ 58__ 58__ 32_ Default_ 32__ 62__ 32__ 58__ 58__ 32_ default - _verus_
external_ ⚠fn_ specification_ 392_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 393_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 394_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 395_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ contains__ key_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 396_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 397_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 398_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 399_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ keys - _verus_
external_ ⚠fn_ specification_ 400_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ values - _verus_
external_ ⚠fn_ specification_ 401_ hash__ set_ 32__ 58__ 58__ 32_ Iter_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 402_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 403_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 404_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 405__ 60__ 32_ Hash Set_ 32__ 60__ 32_ T_ 44__ 32_ S_ 44__ 32__ 62__ 32_ as_ 32_ core_ 32__ 58__ 58__ 32_ default_ 32__ 58__ 58__ 32_ Default_ 32__ 62__ 32__ 58__ 58__ 32_ default - _verus_
external_ ⚠fn_ specification_ 406_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 407_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 408_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 409_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 410_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 411_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 412_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 413_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ iter - axiom_
bool_ obeys_ hash_ table_ key_ model - axiom_
box_ bool_ obeys_ hash_ table_ key_ model - axiom_
box_ integer_ type_ obeys_ hash_ table_ key_ model - axiom_
box_ key_ removed - axiom_
contains_ box - axiom_
contains_ deref_ key - axiom_
deref_ key_ removed - axiom_
hashmap_ decreases - axiom_
hashmap_ deepview_ borrow - axiom_
hashmap_ view_ finite_ dom - axiom_
hashset_ decreases - axiom_
i8_ obeys_ hash_ table_ key_ model - axiom_
i16_ obeys_ hash_ table_ key_ model - axiom_
i32_ obeys_ hash_ table_ key_ model - axiom_
i64_ obeys_ hash_ table_ key_ model - axiom_
i128_ obeys_ hash_ table_ key_ model - axiom_
isize_ obeys_ hash_ table_ key_ model - axiom_
maps_ box_ key_ to_ value - axiom_
maps_ deref_ key_ to_ value - axiom_
random_ state_ builds_ valid_ hashers - axiom_
set_ box_ key_ removed - axiom_
set_ box_ key_ to_ value - axiom_
set_ contains_ box - axiom_
set_ contains_ deref_ key - axiom_
set_ deref_ key_ removed - axiom_
set_ deref_ key_ to_ value - axiom_
spec_ hash_ map_ iter - axiom_
spec_ hash_ map_ len - axiom_
spec_ hash_ set_ len - axiom_
u8_ obeys_ hash_ table_ key_ model - axiom_
u16_ obeys_ hash_ table_ key_ model - axiom_
u32_ obeys_ hash_ table_ key_ model - axiom_
u64_ obeys_ hash_ table_ key_ model - axiom_
u128_ obeys_ hash_ table_ key_ model - axiom_
usize_ obeys_ hash_ table_ key_ model - borrowed_
key_ removed - builds_
valid_ hashers - contains_
borrowed_ key - group_
hash_ axioms - hash_
map_ deep_ view_ impl - lemma_
hashmap_ deepview_ dom - lemma_
hashmap_ deepview_ properties - lemma_
hashmap_ deepview_ values - maps_
borrowed_ key_ to_ value - obeys_
key_ model - set_
contains_ borrowed_ key - sets_
borrowed_ key_ to_ key - sets_
differ_ by_ borrowed_ key - spec_
hash_ map_ iter - spec_
hash_ map_ len - spec_
hash_ set_ len