Challenge 4: Verify memory safety of BTreeMap node module with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for operations in library/alloc/src/collections/btree/node.rs for Challenge 4.

The change introduces:

• contracts for LeafNode::init, including writable-memory preconditions and
  initialization postconditions;
• Kani proof harnesses for node initialization and selected NodeRef,
  Handle, and BalancingContext operations;
• symbolic construction of leaf and internal nodes through the same allocation
  and insertion paths used by the implementation;
• symbolic node lengths, tracked edge indices, and steal counts constrained to
  their legal capacity ranges;
• post-call kani::cover properties for the verified operation paths;
• bounded harnesses for recursive and loop-heavy operations listed by Challenge 4.

No non-verification runtime behavior is changed in normal builds.

Verification Coverage Report

Initialization and basic node operations

The verification module includes harnesses for:

• LeafNode::init
• LeafNode::new
• InternalNode::new
• NodeRef::as_internal_mut
• NodeRef::len
• NodeRef::first_edge
• NodeRef::last_edge
• NodeRef::first_kv
• NodeRef::last_kv
• NodeRef::into_leaf
• NodeRef::keys
• NodeRef::as_leaf_mut
• NodeRef::into_leaf_mut
• NodeRef::as_leaf_dying
• NodeRef::pop_internal_level
• NodeRef::push
• handle navigation and key/value accessors

Recursive and balancing operations

The following Challenge 4 operations have bounded harnesses:

• NodeRef::new_internal
• Handle::insert_recursing
• BalancingContext::do_merge
• BalancingContext::merge_tracking_child_edge
• BalancingContext::steal_left
• BalancingContext::steal_right
• BalancingContext::bulk_steal_left
• BalancingContext::bulk_steal_right

The balancing harnesses use a shared fixture containing an internal parent
with two leaf children. Child lengths are symbolic over the node capacity
range, and each operation constrains its inputs according to the operation's
preconditions:

• merge operations require
  left_len + 1 + right_len <= CAPACITY;
• steal_left requires a non-empty left child and room in the right child;
• steal_right requires a non-empty right child and room in the left child;
• bulk steals use symbolic positive counts bounded by the source child length
  and destination capacity;
• tracked edge indices are symbolic and constrained to the selected child.

Approach

The verification strategy combines contracts with executable bounded harnesses.

1. Contracts for unsafe initialization

   LeafNode::init is verified through proof_for_contract, checking that
   writes target valid memory and establish the required metadata.

2. Shared symbolic fixtures

   Nodes are constructed through new_leaf, new_internal, and push.
   This preserves the implementation's initialization and parent-linking
   behavior instead of fabricating arbitrary raw pointers.

3. Behavioral postconditions

   Harnesses check metadata, pointer relationships, node lengths, returned
   handles, and parent links. kani::cover is placed after the assertions to
   show that the target path is reachable.

4. Bounded verification of recursive operations

   Recursive and loop-heavy operations use bounded unwinding. The harnesses
   cover symbolic legal node occupancies and operation parameters, while
   keeping the fixed node capacity explicit.

Verification

All added Challenge 4 harnesses pass locally with Kani.

Resolves #77

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.