Challenge 4: Memory safety of BTreeMap's btree::node module

• Status: Open
• Tracking Issue: #77
• Start date: 2024/07/01
• End date: 2025/04/10
• Reward: 10,000 USD

Goal

Verify the memory safety of the alloc::collections::btree::node module. This is one of the main modules used for implementing the BTreeMap collection, and it includes a lot of unsafe code.

Success Criteria

The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.:

1. LeafNode::new
2. NodeRef::as_internal_mut
3. NodeRef::len
4. NodeRef::ascend
5. NodeRef::first_edge
6. NodeRef::last_edge
7. NodeRef::first_kv
8. NodeRef::last_kv
9. NodeRef::into_leaf
10. NodeRef::keys
11. NodeRef::as_leaf_mut
12. NodeRef::into_leaf_mut
13. NodeRef::as_leaf_dying
14. NodeRef::pop_internal_level
15. NodeRef::push
16. Handle::left_edge
17. Handle::right_edge
18. Handle::left_kv
19. Handle::right_kv
20. Handle::descend
21. Handle::into_kv
22. Handle::key_mut
23. Handle::into_val_mut
24. Handle::into_kv_mut
25. Handle::into_kv_valmut
26. Handle::kv_mut

Verification must be unbounded for functions that use recursion or contain loops, e.g.

1. NodeRef::new_internal
2. Handle::insert_recursing
3. BalancingContext::do_merge
4. BalancingContext::merge_tracking_child_edge
5. BalancingContext::steal_left
6. BalancingContext::steal_right
7. BalancingContext::bulk_steal_left
8. BalancingContext::bulk_steal_right

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.