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. - ExEntry
- 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 - ExOccupied
Entry - ExRandom
State - Specifications for the behavior of
std::hash::RandomState. - ExSet
Iter - ExVacant
Entry - ExValues
- Specifications for the behavior of
std::collections::hash_map::Values.
Traits§
- Default
Hasher Additional Spec Fns - Entry
Spec Fns - Specification for an
Entry. Contains the current key for the entry, and prophesies the final value after this instantiation of the entry API is complete. - ExBuild
Hasher - ExHasher
- Hash
MapAdditional Spec Fns - Occupied
Entry Spec Fns - Specification for an
OccupiedEntry. Contains the current key and value in the entry, and prophesies the final value after this instantiation of the entry API is complete. The final value is optional, since the user might choose to remove the entry. - Vacant
Entry Spec Fns - Specification for a
VacantEntry. Contains the current key for the entry, and prophesies the final value after this instantiation of the entry API is complete. The final value is optional, since the user may or may not choose to insert a value.
Functions§
- _verus_
external_ ⚠fn_ specification_ 411_ Default Hasher_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 412_ Default Hasher_ 32__ 58__ 58__ 32_ write - _verus_
external_ ⚠fn_ specification_ 413_ Default Hasher_ 32__ 58__ 58__ 32_ finish - _verus_
external_ ⚠fn_ specification_ 414_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 415_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 416_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 417__ 60__ 32_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ K_ 44__ 32_ V_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32_ as_ 32_ Clone_ 32__ 62__ 32__ 58__ 58__ 32_ clone - _verus_
external_ ⚠fn_ specification_ 418_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 419__ 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_ 420_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 421_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 422_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 423_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ contains__ key_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 424_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 425_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 426_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 427_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ keys - _verus_
external_ ⚠fn_ specification_ 428_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ values - _verus_
external_ ⚠fn_ specification_ 429_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 430_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 431_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 432__ 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_ 433_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 434_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ reserve - _verus_
external_ ⚠fn_ specification_ 435_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 436_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 437_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 438_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 439_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 440_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 441_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ entry - _verus_
external_ ⚠fn_ specification_ 442_ Entry_ 32__ 58__ 58__ 32_ key - _verus_
external_ ⚠fn_ specification_ 443_ Entry_ 32__ 58__ 58__ 32_ or__ insert - _verus_
external_ ⚠fn_ specification_ 444_ Entry_ 32__ 58__ 58__ 32_ insert__ entry - _verus_
external_ ⚠fn_ specification_ 445_ Occupied Entry_ 32__ 58__ 58__ 32_ remove__ entry - _verus_
external_ ⚠fn_ specification_ 446_ Occupied Entry_ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 447_ Occupied Entry_ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 448_ Occupied Entry_ 32__ 58__ 58__ 32_ into__ mut - _verus_
external_ ⚠fn_ specification_ 449_ Occupied Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 450_ Occupied Entry_ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 451_ Vacant Entry_ 32__ 58__ 58__ 32_ into__ key - _verus_
external_ ⚠fn_ specification_ 452_ Vacant Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 453_ Vacant Entry_ 32__ 58__ 58__ 32_ insert__ entry - 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_
has_ resolved_ entry - axiom_
has_ resolved_ occupied_ entry - axiom_
has_ resolved_ vacant_ entry - 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_ keys_ iter - axiom_
spec_ hash_ map_ iter - axiom_
spec_ hash_ map_ len - axiom_
spec_ hash_ set_ len - axiom_
spec_ keys_ iter - axiom_
spec_ values_ iter - 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 - into_
iter - into_
iter_ hash_ keys - into_
iter_ keys - into_
iter_ values - 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_ keys_ iter - spec_
hash_ map_ iter - spec_
hash_ map_ len - spec_
hash_ set_ len - spec_
keys_ iter - spec_
values_ iter