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_ 764_ Default Hasher_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 765_ Default Hasher_ 32__ 58__ 58__ 32_ write - _verus_
external_ ⚠fn_ specification_ 766_ Default Hasher_ 32__ 58__ 58__ 32_ finish - _verus_
external_ ⚠fn_ specification_ 767_ 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_ 768_ 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_ 769_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ capacity - _verus_
external_ ⚠fn_ specification_ 770_ 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_ 771__ 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_ 772_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 773__ 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_ 774_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 775_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ with__ hasher - _verus_
external_ ⚠fn_ specification_ 776_ 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_ 777_ 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_ 778_ 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_ 779_ 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_ 780_ 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_ 781_ 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_ 782_ 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_ 783_ 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_ 784_ 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_ 785_ 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_ 786_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 787__ 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_ 788_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 789_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ with__ hasher - _verus_
external_ ⚠fn_ specification_ 790_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity__ and__ hasher - _verus_
external_ ⚠fn_ specification_ 791_ 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_ 792_ 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_ 793_ 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_ 794_ 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_ 795_ 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_ 796_ 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_ 797_ 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_ 798_ 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_ 799_ Entry_ 32__ 58__ 58__ 32_ key - _verus_
external_ ⚠fn_ specification_ 800_ Entry_ 32__ 58__ 58__ 32_ or__ insert - _verus_
external_ ⚠fn_ specification_ 801_ Entry_ 32__ 58__ 58__ 32_ insert__ entry - _verus_
external_ ⚠fn_ specification_ 802_ Occupied Entry_ 32__ 58__ 58__ 32_ remove__ entry - _verus_
external_ ⚠fn_ specification_ 803_ Occupied Entry_ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 804_ Occupied Entry_ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 805_ Occupied Entry_ 32__ 58__ 58__ 32_ into__ mut - _verus_
external_ ⚠fn_ specification_ 806_ Occupied Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 807_ Occupied Entry_ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 808_ Vacant Entry_ 32__ 58__ 58__ 32_ into__ key - _verus_
external_ ⚠fn_ specification_ 809_ Vacant Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 810_ 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_ 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 - 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_ map_ len - spec_
hash_ set_ len