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_ 561_ Default Hasher_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 562_ Default Hasher_ 32__ 58__ 58__ 32_ write - _verus_
external_ ⚠fn_ specification_ 563_ Default Hasher_ 32__ 58__ 58__ 32_ finish - _verus_
external_ ⚠fn_ specification_ 564_ 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_ 565_ 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_ 566_ 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_ 567__ 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_ 568_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 569__ 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_ 570_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 571_ 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_ 572_ 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_ 573_ 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_ 574_ 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_ 575_ 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_ 576_ 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_ 577_ 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_ 578_ 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_ 579_ 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_ 580_ 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_ 581_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 582__ 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_ 583_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 584_ 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_ 585_ 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_ 586_ 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_ 587_ 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_ 588_ 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_ 589_ 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_ 590_ 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_ 591_ 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_ 592_ Entry_ 32__ 58__ 58__ 32_ key - _verus_
external_ ⚠fn_ specification_ 593_ Entry_ 32__ 58__ 58__ 32_ or__ insert - _verus_
external_ ⚠fn_ specification_ 594_ Entry_ 32__ 58__ 58__ 32_ insert__ entry - _verus_
external_ ⚠fn_ specification_ 595_ Occupied Entry_ 32__ 58__ 58__ 32_ remove__ entry - _verus_
external_ ⚠fn_ specification_ 596_ Occupied Entry_ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 597_ Occupied Entry_ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 598_ Occupied Entry_ 32__ 58__ 58__ 32_ into__ mut - _verus_
external_ ⚠fn_ specification_ 599_ Occupied Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 600_ Occupied Entry_ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 601_ Vacant Entry_ 32__ 58__ 58__ 32_ into__ key - _verus_
external_ ⚠fn_ specification_ 602_ Vacant Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 603_ 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_
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