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.

[feliperodri]

Thanks @v3risec. Reviewed against Challenge 4. This is much stronger than the other Ch4 attempts — 26/26 listed base fns each with a dedicated harness, all 8 recursion/balancing fns present, symbolic occupancy (len = kani::any_where(|l| *l <= CAPACITY) with symbolic keys/values built through the real push path), and #[kani::unwind(13)] fully unwinds the ≤12-edge relink loops — so for the CAPACITY-bounded loops a full-occupancy symbolic harness is genuinely complete. Clean soundness: no cfg body swaps, no trivial invariants, the one contract (LeafNode::init) has a matching proof_for_contract, no assume-the-conclusion.

Requesting changes on two real coverage gaps versus the criteria:

1. insert_recursing recursion is never exercised. harness_insert_recursing inserts into an empty leaf root with spare capacity, so self.insert returns (None, handle) and returns before the loop (node.rs:1068) — your own comment says "completed without splitting." The recursive/splitting path (the whole point of listing it as an unbounded fn) is dead. Please drive a full node that forces a split and ascends.
2. Balancing fns cover the leaf arm only. do_merge, merge_tracking_child_edge, steal_left/right, bulk_steal_left/right build new_leaf children, so the internal-node edge-array-copy + parent-relink arm is never taken. (#666's full-occupancy internal do_merge harness is worth borrowing for this.)

This is the prioritized Ch4 solution — close those two gaps (recursion + internal-node balancing arms) and it's approvable. Nice work on the symbolic-occupancy fixtures.

[ivmat]

@v3risec #666 is closed but as feliperodri mentioned, please see if you could reuse do_merge harness from the PR

[v3risec]

@feliperodri Thanks for the detailed review and suggestions. I’m currently working on the requested changes, in particular exercising the recursive/splitting path in insert_recursing and adding coverage for the internal-node balancing paths.

@ivmat Thanks for the guidance! I’ll take a closer look at the do_merge harness from #666 and reuse/adapt the relevant parts. Thanks again!