Challenge 4: bounded Kani PROBEs on btree::node's copy, relink and rebalancing helpers

[ivmat]

This extends the previous nine-harness entry to twenty-eight, adding the rebalancing family named in
the challenge's second success-criteria list, the functional-content companions for
Handle::move_suffix, and Handle::split.

It remains a bounded PROBE set, not a discharge of the challenge: every harness is monomorphic at
K = V = i32, and tree height is bounded. What has changed is coverage — seven of the eight
functions in the second list are now driven directly — and strength: several claims that the previous
entry recorded as open residuals are now proven.

The challenge's criterion is memory safety, and Kani emits its UB checks on every path whether or
not an assertion is written. The functional content assertions here are therefore additional to the
criterion, not a substitute for it.

What is proved

area	harnesses	note
Handle::move_suffix content	6	post-state content of both nodes after the type-erasure + two-node copy, read back through Handle::new_kv(..).into_kv(), plus a raw stored-length diagnostic
NodeRef::new_internal	1	both child shapes (leaf child → height 1, internal child → height 2)
correct_all_childrens_parent_links	1	over the complete occupancy domain
Handle::split (leaf arm)	1	the whole function, including the node it allocates; the internal-node split is not driven
do_merge	3	leaf arm over the complete occupancy domain; internal arm with content assertions at a stated bound; internal arm with child occupancies constrained only by do_merge's own precondition, memory safety
bulk_steal_left / bulk_steal_right	4	leaf arm over the complete occupancy domain, plus both internal arms
steal_left / steal_right / merge_tracking_child_edge	3	the three wrappers, each driven directly
previous entry, unchanged	9	insert_fit, remove, move_suffix safety, the two relink harnesses

Second success-criteria list: 7 of 8 functions harnessed — new_internal, do_merge,
merge_tracking_child_edge, steal_left, steal_right, bulk_steal_left, bulk_steal_right.
Six are called directly by a harness; do_merge is driven through its own public wrapper
merge_tracking_parent, which is the real call path rather than a re-implementation.
insert_recursing is not included; see residuals.

The two bulk_steal_* leaf-arm harnesses assert their destination/source stored length and
their key-and-value shift, rather than recording them as coverage witnesses.

Scope and method

Fixtures use K = V = i32 and the module's own CAPACITY (11, for B = 6). Content is
position-derived ((i, 1000 + i)) where a misplaced write must be observable. Node lengths, split
indices, edge ranges and steal counts are symbolic — except in the move_suffix family, whose
source length is sampled at {0, 1, CAPACITY}, and Handle::split, sampled at {1, CAPACITY}.

On "symbolic len over 0..=CAPACITY". CAPACITY is a compile-time constant and a
LeafNode<K, V> stores keys: [MaybeUninit<K>; CAPACITY], so a node's occupancy cannot exceed it in
any reachable state. A harness that leaves len symbolic across 0..=CAPACITY is therefore
verifying the node type's complete occupancy domain, not a chosen slice of it. The same holds for
the count argument of bulk_steal_* and for every loop whose trip count derives from a node
length.

Bounds that are harness-chosen are called out individually in the source and in the residuals
below: the internal-arm occupancy bound IB (the fixture must materialise IB + 1 grandchildren by
hand), and tree height.

Non-vacuity is carried by kani::cover witnesses on every harness — interior versus boundary split
points, empty versus maximal children, count == 1 versus a genuine bulk steal, and the shapes that
make each relink loop iterate more than once. Replay-greens are defeated per harness: parent links
are perturbed to a sentinel before the relink harnesses run, and content harnesses use
position-derived values so a misplaced write is observable.

What is NOT proved

Each residual below was measured at Kani 0.67.0 / CBMC 6.8.0, the toolchain this entry pins. Most
of them — monomorphisation, bounded height, the harness-chosen IB, the fixed parent shape, and
per-index readback — are properties of the harness design and would hold at any pin. The previous
entry's two residuals, by contrast, WERE toolchain properties, and are retired below. The pin is
stated throughout so a reader can tell the two kinds apart.

• The challenge's unboundedness requirement is not discharged for ANY of the eight functions.
  That requirement heads the whole second list, not just one entry. These are bounded probes. The
  occupancy axis happens to be bounded by the node type itself, which makes the child-length bounds
  non-artificial, but height, parent shape and monomorphisation remain harness bounds throughout.
• insert_recursing is not harnessed in this entry at all. Its loop ascends from the insertion
  point to the root, so its trip count is the tree's height — the one axis the node type does not
  bound, unlike occupancy. Harnessing it at a fixed height is possible, but a bounded-height result
  would not discharge the requirement for it, so it is left out rather than shipped with a bound that
  reads stronger than it is.
• Generic K and V are not covered. Every harness is monomorphic at i32/i32; nothing here
  is proven for arbitrary K: Ord or V.
• Tree height is bounded. Leaf-arm harnesses use a height-1 parent; internal-arm harnesses use a
  height-2 tree. Nothing here speaks to deeper trees.
• The internal-arm occupancy bound IB is harness-chosen on the content-carrying internal
  harnesses (IB = 2), because the fixture materialises IB + 1 grandchildren explicitly. In
  check_do_merge_internal_full_occupancy_no_ub the fixture cap is raised to CAPACITY and is
  deliberately non-binding: do_merge's own precondition (old_left_len + 1 + right_len <= CAPACITY) is what constrains the children there, so no single child reaches CAPACITY pre-merge —
  the reachable maximum is CAPACITY - 1 with the other child empty.
• The parent's own shape is fixed. Every balancing harness uses a parent of one or two pairs and
  operates at parent index 0; do_merge's parent-side gap-close and relink therefore run at trip
  counts 0–1 only.
• Functional readback is per-index, not simultaneous. The relink harnesses check one symbolic
  child index per run and the content harnesses check named boundary positions; neither asserts the
  property for all positions at once. Kani's memory-safety checks are all-paths regardless, which is
  what the challenge's criterion asks for.

On the previous entry's two disclosed limitations — a suspected CBMC pointer-model residual on the
move_suffix content readback, and a deferred do_merge/bulk_steal unwind hang — both were
measured on Kani 0.65.0 / CBMC 6.7.1. Re-measured on this entry's pin they do not reproduce: the
move_suffix content family and the whole rebalancing family discharge, and those harnesses are
included above. The earlier limitations were specific to the older toolchain and are not carried
forward.

Toolchain and reproduction

• kani 0.67.0, built from source at d4df833c8f8f18e632e7b0a7945bb2161f708990
• CBMC 6.8.0 (this pin's own kani-dependencies)

kani verify-std -Z unstable-options ./library \
  -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts \
  -Z quantifiers -Z stubbing --no-assert-contracts --harness <harness-name> \
  --cbmc-args --object-bits 12

One run, one sha: every row below comes from a single whole-set run at the submitted commit, on a
16-vCPU / 128 GB VM. 28 of 28 SUCCESSFUL, 83/83 cover properties satisfied.

harness	verdict	covers	maxRSS	wall
check_correct_all_childrens_parent_links_no_ub	SUCCESSFUL	3/3	4.3 GB	1:34.96
check_correct_childrens_parent_links_subrange_no_ub	SUCCESSFUL	6/6	4.7 GB	2:56.90
check_leaf_insert_fit_no_ub	SUCCESSFUL	2/2	1.7 GB	0:52.75
check_leaf_insert_fit_content	SUCCESSFUL	1/1	1.6 GB	0:53.72
check_internal_insert_fit_no_ub	SUCCESSFUL	2/2	5.7 GB	5:23.97
check_internal_insert_fit_content	SUCCESSFUL	2/2	9.6 GB	8:09.53
check_leaf_remove_no_ub	SUCCESSFUL	3/3	1.7 GB	0:58.82
check_leaf_remove_content	SUCCESSFUL	1/1	1.7 GB	0:53.00
check_move_suffix_leaf_no_ub	SUCCESSFUL	3/3	1.6 GB	0:41.16
check_move_suffix_leaf_raw_len	SUCCESSFUL	3/3	1.6 GB	0:44.26
check_move_suffix_leaf_content_all	SUCCESSFUL	1/1	1.7 GB	0:47.15
check_move_suffix_leaf_content_check_a	SUCCESSFUL	1/1	1.7 GB	0:45.16
check_move_suffix_leaf_content_check_b	SUCCESSFUL	1/1	1.7 GB	0:45.83
check_move_suffix_leaf_content_check_c	SUCCESSFUL	1/1	1.7 GB	0:44.79
check_move_suffix_leaf_content_check_d	SUCCESSFUL	1/1	1.7 GB	0:44.07
check_leaf_split_no_ub	SUCCESSFUL	3/3	1.7 GB	0:55.05
check_new_internal_no_ub	SUCCESSFUL	2/2	1.6 GB	0:47.74
check_correct_all_childrens_parent_links_full_domain	SUCCESSFUL	4/4	4.7 GB	2:31.05
check_steal_left_leaf_no_ub	SUCCESSFUL	3/3	6.0 GB	2:02.56
check_steal_right_leaf_no_ub	SUCCESSFUL	3/3	3.3 GB	1:20.93
check_merge_tracking_child_edge_leaf_no_ub	SUCCESSFUL	3/3	3.9 GB	2:29.45
check_do_merge_leaf_no_ub	SUCCESSFUL	6/6	4.7 GB	3:48.25
check_bulk_steal_left_leaf_scoped_no_ub	SUCCESSFUL	5/5	5.9 GB	7:03.20
check_bulk_steal_right_leaf_scoped_no_ub	SUCCESSFUL	6/6	5.9 GB	4:35.61
check_bulk_steal_left_internal_no_ub	SUCCESSFUL	4/4	26.5 GB	7:04.36
check_bulk_steal_right_internal_no_ub	SUCCESSFUL	4/4	23.8 GB	5:53.22
check_do_merge_internal_no_ub	SUCCESSFUL	5/5	14.5 GB	10:25.97
check_do_merge_internal_full_occupancy_no_ub	SUCCESSFUL	4/4	18.2 GB	16:04.71

Controls

Four claims are backed by an observed-red mutation control: a single-token length mutation is applied
to the implementation, and the harness that owns the claim is required to go RED. All four did.

mutant	what it breaks	harness required to go RED	observed
M1	move_suffix's destination stored length	check_move_suffix_leaf_raw_len, check_move_suffix_leaf_content_all	RED
M2	do_merge's merged-child stored length	check_do_merge_leaf_no_ub	RED
M3	bulk_steal_left's destination stored length	check_bulk_steal_left_leaf_scoped_no_ub	RED
M4	bulk_steal_right's source stored length	check_bulk_steal_right_leaf_scoped_no_ub	RED

The mutations are applied on the verification machine only and are not part of this diff: an in-tree
#[kani::proof] designed to fail would turn any whole-set run of the submission red.

Acceptance manifest

A machine-readable statement of exactly what these proofs establish and do not establish — one entry
per claim, with declared bounds, evidence, and assurance band, checked by a standalone validator — is
shipped as a real-world example in the format's own repo:
examples/verify-rust-std-ch4-btree-v2/acceptance.toml
(format). It records 13 claims: 12 evidence-bearing
(four graded A3 — each with a red mutation control naming the claim — the rest A0) and one
explicit gap entry for what this PR does not prove (insert_recursing is not harnessed; and no
claim asserts any unboundedness requirement). Stamped and verified at this branch's head (9a083f4bc12).