Expand description
This code adds specifications for the standard-library types
std::collections::BTreeMap and std::collections::BTreeSet.
The specification is only meaningful when the Key obeys our Ord model,
as specified by super::super::laws_cmp::obeys_cmp_spec.
By default, the Verus standard library brings useful axioms
about the behavior of BTreeMap and BTreeSet into the ambient
reasoning context by broadcasting the group
vstd::std_specs::btree::group_btree_axioms.
Structs§
- ExBTree
Map - Specifications for the behavior of
std::collections::BTreeMap. - ExBTree
Set - Specifications for the behavior of
std::collections::BTreeSet. - ExKeys
- Specifications for the behavior of
std::collections::btree_map::Keys. - ExMap
Iter - ExSet
Iter - ExValues
- Specifications for the behavior of
std::collections::btree_map::Values. - Keys
Ghost Iterator - MapIter
Ghost Iterator - SetIter
Ghost Iterator - Values
Ghost Iterator
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 414_ 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_ 415_ 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_ 416_ btree__ map_ 32__ 58__ 58__ 32_ Iter_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ K_ 44__ 32_ V_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 417_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ iter - _verus_
external_ ⚠fn_ specification_ 418_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 419_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 420__ 60__ 32_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ K_ 44__ 32_ V_ 44__ 32_ A_ 44__ 32__ 62__ 32_ as_ 32_ Clone_ 32__ 62__ 32__ 58__ 58__ 32_ clone - _verus_
external_ ⚠fn_ specification_ 421_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 422__ 60__ 32_ BTree Map_ 32__ 60__ 32_ K_ 44__ 32_ V_ 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_ 423_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 424_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ contains__ key_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 425_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 426_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 427_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 428_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ keys - _verus_
external_ ⚠fn_ specification_ 429_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ values - _verus_
external_ ⚠fn_ specification_ 430_ btree__ 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_ 431_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 432_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 433__ 60__ 32_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ K_ 44__ 32_ A_ 32__ 62__ 32_ as_ 32_ Clone_ 32__ 62__ 32__ 58__ 58__ 32_ clone - _verus_
external_ ⚠fn_ specification_ 434_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 435__ 60__ 32_ BTree Set_ 32__ 60__ 32_ T_ 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_ 436_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 437_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 438_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 439_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ remove_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 440_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 441_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ iter - axiom_
box_ key_ removed - axiom_
btree_ map_ decreases - axiom_
btree_ map_ deepview_ borrow - axiom_
btree_ map_ view_ finite_ dom - axiom_
btree_ set_ decreases - axiom_
contains_ box - axiom_
contains_ deref_ key - axiom_
deref_ key_ removed - axiom_
increasing_ seq_ meaning - axiom_
key_ obeys_ cmp_ spec_ meaning - axiom_
maps_ box_ key_ to_ value - axiom_
maps_ deref_ key_ to_ value - 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_ btree_ map_ iter - axiom_
spec_ btree_ map_ len - axiom_
spec_ btree_ set_ len - borrowed_
key_ removed - btree_
map_ deep_ view_ impl - contains_
borrowed_ key - group_
btree_ axioms - increasing_
seq - key_
obeys_ cmp_ spec - lemma_
btree_ map_ deepview_ dom - lemma_
btree_ map_ deepview_ properties - lemma_
btree_ map_ deepview_ values - maps_
borrowed_ key_ to_ value - set_
contains_ borrowed_ key - sets_
borrowed_ key_ to_ key - sets_
differ_ by_ borrowed_ key - spec_
btree_ map_ iter - spec_
btree_ map_ len - spec_
btree_ set_ len