Implement BoundedArbitrary for BTreeMap and BTreeSet#4626
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
hz2
force-pushed
the
bounded-arbitrary-btree
branch
from
4a72a28 to
41da7be
Compare
Add BoundedArbitrary implementations for BTreeMap<K, V> and BTreeSet<V>,
following the same pattern as the existing HashMap and HashSet impls.
BTreeMap and BTreeSet operations cause state-space explosion during
verification due to tree rebalancing internals. Providing a bounded
constructor via BoundedArbitrary gives users an idiomatic way to generate
symbolic BTree collections with controlled size.
Usage:
let map: BTreeMap<u8, bool> = kani::bounded_any::<_, 4>();
hz2
force-pushed
the
bounded-arbitrary-btree
branch
from
41da7be to
8e142d8
Compare
There was a problem hiding this comment.
Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| { | ||
| fn bounded_any<const N: usize>() -> Self { | ||
| let mut btree_map = std::collections::BTreeMap::new(); | ||
| for _ in 0..N { |
There was a problem hiding this comment.
Non-blocking: Nice parity with the HashMap bounded generator pattern. Could we add a short comment here noting that duplicate K::any() values may overwrite entries, so reachable map sizes are in 0..=N (not necessarily equal to number of successful insert branches)? It may help future readers understand why size coverage still works as expected.
| { | ||
| fn bounded_any<const N: usize>() -> Self { | ||
| let mut btree_set = std::collections::BTreeSet::new(); | ||
| for _ in 0..N { |
There was a problem hiding this comment.
Non-blocking: Same thought as map: a brief note that duplicate V::any() values can collapse cardinality would make the bounded-size behavior explicit for BTreeSet.
| #[kani::unwind(5)] | ||
| fn check_btreemap() { | ||
| const BOUND: usize = 2; | ||
| let btree_map: std::collections::BTreeMap<u8, bool> = kani::bounded_any::<_, BOUND>(); |
There was a problem hiding this comment.
Non-blocking: Consider adding assert!(btree_map.len() <= BOUND); as an explicit invariant check. The cover! checks already show reachability of 0/1/2, but this makes the upper-bound contract very obvious in the harness.
| #[kani::unwind(5)] | ||
| fn check_btreeset() { | ||
| const BOUND: usize = 2; | ||
| let btree_set: std::collections::BTreeSet<u8> = kani::bounded_any::<_, BOUND>(); |
There was a problem hiding this comment.
Non-blocking: Optional consistency nit: add assert!(btree_set.len() <= BOUND); to mirror the bounded invariant explicitly for the set harness too.
|
@hz2 don't forget to update the branch and address all CI issues before merging. Thanks for the contribution! 🦀 |
Summary
BoundedArbitraryimplementations forBTreeMap<K, V>andBTreeSet<V>HashMapandHashSetimpls inlibrary/kani/src/bounded_arbitrary.rstests/expected/bounded-arbitrary/btree/Motivation
BTreeMap and BTreeSet operations cause state-space explosion during verification due to tree rebalancing internals (see #1251, #3965). Users currently have no idiomatic way to generate bounded symbolic BTree collections.
The existing
BoundedArbitraryimpls coverVec,Box<[T]>,String,HashMap, andHashSet-- butBTreeMapandBTreeSetare absent despite being commonly used in Rust codebases.This addition lets users write:
Testing
Added
tests/expected/bounded-arbitrary/btree/btree.rswith cover property checks for sizes 0, 1, and 2 on bothBTreeMapandBTreeSet, matching the structure oftests/expected/bounded-arbitrary/hash/hash.rs.Related issues: #1251, #3965