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 unless you assume
builds_valid_hashers<CustomBuildHasher>().
Likewise, the specification is only meaningful when eq_spec
faithfully models executable equality; executable equality is
reflexive, symmetric, and transitive; hashing is
deterministic; executable-equal keys hash identically; and
cloning, when supported, preserves structural identity and
executable equality. 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.
The assumed specs don’t assume that executable equality matches structural equality, or that executable equality matches deep_view equality. But we provide broadcast lemmas that derive stronger properties for when either of those do match.
Borrowed-key lookups also require
borrowed_key_hashing_matches::<Key, Q>() and use the model in
BorrowSpec. Their postconditions additionally require Q to obey
the hashing and equality models. Compatibility is supplied for identity,
reference, Box, and String borrowing.
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
Into Iter - 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 - 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_ 778_ Default Hasher_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 779_ Default Hasher_ 32__ 58__ 58__ 32_ write - _verus_
external_ ⚠fn_ specification_ 780_ Default Hasher_ 32__ 58__ 58__ 32_ finish - _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_ iter - _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_ into__ iter - _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_ len - _verus_
external_ ⚠fn_ specification_ 784_ 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_ 785_ 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_ 786__ 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_ 787_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 788__ 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_ 789_ Hash Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 790_ 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_ 791_ 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_ 792_ 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_ 793_ 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_ 794_ 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_ 795_ 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_ 796_ 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_ 797_ 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_ 798_ 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_ 799_ 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_ 800_ 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_ 801_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 802__ 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_ 803_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ with__ capacity - _verus_
external_ ⚠fn_ specification_ 804_ Hash Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ S_ 32__ 62__ 32__ 58__ 58__ 32_ with__ hasher - _verus_
external_ ⚠fn_ specification_ 805_ 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_ 806_ 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_ 807_ 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_ 808_ 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_ 809_ 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_ 810_ 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_ 811_ 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_ 812_ 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_ 813_ 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_ 814_ Entry_ 32__ 58__ 58__ 32_ key - _verus_
external_ ⚠fn_ specification_ 815_ Entry_ 32__ 58__ 58__ 32_ or__ insert - _verus_
external_ ⚠fn_ specification_ 816_ Entry_ 32__ 58__ 58__ 32_ insert__ entry - _verus_
external_ ⚠fn_ specification_ 817_ Occupied Entry_ 32__ 58__ 58__ 32_ remove__ entry - _verus_
external_ ⚠fn_ specification_ 818_ Occupied Entry_ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 819_ Occupied Entry_ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 820_ Occupied Entry_ 32__ 58__ 58__ 32_ into__ mut - _verus_
external_ ⚠fn_ specification_ 821_ Occupied Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 822_ Occupied Entry_ 32__ 58__ 58__ 32_ remove - _verus_
external_ ⚠fn_ specification_ 823_ Vacant Entry_ 32__ 58__ 58__ 32_ into__ key - _verus_
external_ ⚠fn_ specification_ 824_ Vacant Entry_ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 825_ Vacant Entry_ 32__ 58__ 58__ 32_ insert__ entry - axiom_
bool_ obeys_ hash_ table_ key_ model - axiom_
borrowed_ key_ hashing_ matches_ box - axiom_
borrowed_ key_ hashing_ matches_ ref - axiom_
borrowed_ key_ hashing_ matches_ self - axiom_
borrowed_ key_ hashing_ matches_ string - axiom_
box_ bool_ obeys_ hash_ table_ key_ model - axiom_
box_ integer_ type_ obeys_ hash_ table_ key_ model - axiom_
has_ resolved_ entry - axiom_
has_ resolved_ occupied_ entry - axiom_
has_ resolved_ vacant_ entry - axiom_
hashmap_ decreases - 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_
key_ model_ implies_ obeys_ eq - axiom_
random_ state_ builds_ valid_ hashers - axiom_
spec_ hash_ map_ len - axiom_
spec_ hash_ set_ len - axiom_
str_ obeys_ hash_ table_ key_ model - axiom_
string_ obeys_ hash_ table_ key_ model - 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_ hashing_ matches - builds_
valid_ hashers - group_
hash_ axioms - hash_
map_ contains_ key_ ensures - hash_
map_ deep_ view_ impl - hash_
map_ entry_ ensures - hash_
map_ get_ ensures - hash_
map_ insert_ ensures - hash_
map_ inv - hash_
map_ remove_ ensures - hash_
set_ contains_ ensures - hash_
set_ get_ ensures - hash_
set_ insert_ ensures - hash_
set_ inv - hash_
set_ remove_ ensures - into_
iter - into_
iter_ entries - into_
iter_ hash_ keys - into_
iter_ keys - into_
iter_ values - lemma_
hash_ map_ contains_ key_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ map_ contains_ key_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ map_ entry_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ map_ entry_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ map_ get_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ map_ get_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ map_ insert_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ map_ insert_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ map_ remove_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ map_ remove_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ set_ contains_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ set_ contains_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ set_ get_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ set_ get_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ set_ insert_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ set_ insert_ ensures_ if_ obeys_ deep_ eq - lemma_
hash_ set_ remove_ ensures_ if_ obeys_ concrete_ eq - lemma_
hash_ set_ remove_ ensures_ if_ obeys_ deep_ eq - lemma_
hashmap_ deepview_ dom - lemma_
hashmap_ deepview_ properties - lemma_
hashmap_ deepview_ values - lemma_
key_ model_ implies_ obeys_ eq - obeys_
key_ model - spec_
hash_ map_ len - spec_
hash_ set_ len