Implement BoundedArbitrary for BTreeMap and BTreeSet

library/kani/src/bounded_arbitrary.rs

@@ -76,3 +76,38 @@ where
         hash_set
     }
 }
+
+impl<K, V> BoundedArbitrary for std::collections::BTreeMap<K, V>
+where
+    K: Arbitrary + std::cmp::Ord,
+    V: Arbitrary,
+{
+    // duplicate `K::any()` values overwrite earlier entries, so the reachable
+    // map sizes are `0..=N` rather than always equal to the number of insert branches taken
+    fn bounded_any<const N: usize>() -> Self {
+        let mut btree_map = std::collections::BTreeMap::new();
+        for _ in 0..N {
+            if bool::any() {
+                btree_map.insert(K::any(), V::any());
+            }
+        }
+        btree_map
+    }
+}
+
+impl<V> BoundedArbitrary for std::collections::BTreeSet<V>
+where
+    V: Arbitrary + std::cmp::Ord,
+{
+    // duplicate `V::any()` values collapse into one entry, so the reachable
+    // set sizes are `0..=N` rather than always equal to the number of insert branches taken
+    fn bounded_any<const N: usize>() -> Self {
+        let mut btree_set = std::collections::BTreeSet::new();
+        for _ in 0..N {
+            if bool::any() {
+                btree_set.insert(V::any());
+            }
+        }
+        btree_set
+    }
+}

tests/expected/bounded-arbitrary/btree/btree.expected

@@ -0,0 +1,10 @@
+Checking harness check_btreeset...
+
+ ** 3 of 3 cover properties satisfied
+
+Checking harness check_btreemap...
+
+ ** 3 of 3 cover properties satisfied
+
+Manual Harness Summary:
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/expected/bounded-arbitrary/btree/btree.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This file tests whether we can generate a bounded BTreeMap/BTreeSet that has any possible size between 0-BOUND
+
+#[kani::proof]
+#[kani::unwind(5)]
+fn check_btreemap() {
+    const BOUND: usize = 2;
+    let btree_map: std::collections::BTreeMap<u8, bool> = kani::bounded_any::<_, BOUND>();
+    assert!(btree_map.len() <= BOUND);
+    kani::cover!(btree_map.len() == 0);
+    kani::cover!(btree_map.len() == 1);
+    kani::cover!(btree_map.len() == 2);
+}
+
+#[kani::proof]
+#[kani::unwind(5)]
+fn check_btreeset() {
+    const BOUND: usize = 2;
+    let btree_set: std::collections::BTreeSet<u8> = kani::bounded_any::<_, BOUND>();
+    assert!(btree_set.len() <= BOUND);
+    kani::cover!(btree_set.len() == 0);
+    kani::cover!(btree_set.len() == 1);
+    kani::cover!(btree_set.len() == 2);
+}