Expand description
This code adds specifications for the standard-library types
alloc::collections::BTreeMap and alloc::collections::BTreeSet.
The specification is only meaningful when the Key obeys our Ord model,
as specified by super::super::laws_cmp::obeys_cmp_spec.
Borrowed-query comparison guarantees additionally require
obeys_cmp::<&Q>() and
<Key as BorrowSpec<Q>>::obeys_borrow_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.
Re-exports§
pub use super::cmp::borrowed_key_ordering_matches;
Structs§
- Cursor
MutModel - The abstract state of a mutable B-tree cursor.
- ExBTree
Map - Specifications for the behavior of
alloc::collections::BTreeMap. - ExBTree
Set - Specifications for the behavior of
alloc::collections::BTreeSet. - ExCursor
Mut - Verus declaration for Rust’s mutable B-tree cursor type.
- ExKeys
- Specifications for the behavior of
alloc::collections::btree_map::Keys. - ExMap
Iter - ExSet
Iter - ExUnordered
KeyError - Verus declaration for the error returned when a cursor insertion would break key ordering.
- ExValues
- Specifications for the behavior of
alloc::collections::btree_map::Values.
Traits§
- BTree
MapAdditional Spec Fns - Cursor
MutSpec Fns - Abstract and prophetic state for mutable B-tree cursors.
Functions§
- _verus_
external_ ⚠fn_ specification_ 745_ 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_ 746_ 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_ 747_ 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_ 748__ 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_ 749_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 750__ 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_ 751_ 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_ 752_ 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_ 753_ 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_ 754_ 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_ 755_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 756_ 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_ 757_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ lower__ bound__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 758_ BTree Map_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ upper__ bound__ mut_ 32__ 58__ 58__ 32__ 60__ 32_ Q_ 32__ 62_ - _verus_
external_ ⚠fn_ specification_ 759_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ next - _verus_
external_ ⚠fn_ specification_ 760_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ prev - _verus_
external_ ⚠fn_ specification_ 761_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ peek__ prev - _verus_
external_ ⚠fn_ specification_ 762_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ peek__ next - _verus_
external_ ⚠fn_ specification_ 763_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ insert__ after - _verus_
external_ ⚠fn_ specification_ 764_ Cursor Mut_ 32__ 58__ 58__ 32__ 60__ 32__ 39_ a_ 44__ 32_ Key_ 44__ 32_ Value_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ remove__ next - _verus_
external_ ⚠fn_ specification_ 765_ 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_ 766_ 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_ 767_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 768_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 769__ 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_ 770_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 32__ 62__ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 771__ 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_ 772_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ insert - _verus_
external_ ⚠fn_ specification_ 773_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 44__ 32__ 62__ 32__ 58__ 58__ 32_ contains - _verus_
external_ ⚠fn_ specification_ 774_ 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_ 775_ 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_ 776_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 777_ BTree Set_ 32__ 58__ 58__ 32__ 60__ 32_ Key_ 44__ 32_ A_ 32__ 62__ 32__ 58__ 58__ 32_ iter - axiom_
btree_ map_ decreases - axiom_
btree_ set_ decreases - axiom_
has_ resolved_ cursor - axiom_
increasing_ seq_ meaning - axiom_
key_ obeys_ cmp_ spec_ meaning - axiom_
spec_ btree_ map_ len - axiom_
spec_ btree_ set_ len - before_
lower_ bound - before_
upper_ bound - btree_
map_ contains_ key_ ensures - btree_
map_ deep_ view_ impl - btree_
map_ get_ ensures - btree_
map_ get_ mut_ ensures - btree_
map_ insert_ ensures - btree_
map_ inv - btree_
map_ remove_ ensures - btree_
set_ contains_ ensures - btree_
set_ get_ ensures - btree_
set_ insert_ ensures - btree_
set_ inv - btree_
set_ remove_ ensures - group_
btree_ axioms - increasing_
seq - into_
iter - into_
iter_ btree_ keys - into_
iter_ keys - into_
iter_ values - key_
fits_ at_ position - key_
obeys_ cmp_ spec - lemma_
btree_ map_ contains_ key_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ map_ contains_ key_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ map_ deepview_ dom - lemma_
btree_ map_ deepview_ properties - lemma_
btree_ map_ deepview_ values - lemma_
btree_ map_ get_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ map_ get_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ map_ get_ mut_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ map_ get_ mut_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ map_ insert_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ map_ insert_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ map_ remove_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ map_ remove_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ set_ contains_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ set_ contains_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ set_ get_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ set_ get_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ set_ insert_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ set_ insert_ ensures_ if_ obeys_ cmp_ deep_ eq - lemma_
btree_ set_ remove_ ensures_ if_ obeys_ cmp_ concrete_ eq - lemma_
btree_ set_ remove_ ensures_ if_ obeys_ cmp_ deep_ eq - positioned_
at_ lower_ bound - positioned_
at_ upper_ bound - spec_
btree_ map_ len - spec_
btree_ set_ len