Verify safety of slice iterator functions with Kani (Challenge 18)

[jrey8343]

Summary

52 Kani proof harnesses verifying safety of slice iterator functions in library/core/src/slice/iter.rs and iter/macros.rs, covering Part 1 (macro-generated functions) and Part 2 (direct iterator implementations).

Part 1: Macro Functions (Iter/IterMut)

Function	Iter	IterMut
next	✅	✅
next_back	✅	✅
nth	✅	—
nth_back	✅	—
advance_by	✅	—
advance_back_by	✅	—
len	✅	—
is_empty	✅	—
size_hint	✅	—
count	✅	—
fold	✅	✅
for_each	✅	✅
position	✅	✅
rposition	✅	—
last	—	—

Part 2: Iterator Type Functions

Type	Functions Covered
Iter	new, clone, default, as_slice, as_ref, post_inc_start, pre_dec_end, next_back_unchecked
IterMut	new, into_slice, as_mut_slice
Split	next, next_back
Chunks	next, next_back, __iterator_get_unchecked
ChunksMut	next, nth, next_back, nth_back, __iterator_get_unchecked
ChunksExact	new, __iterator_get_unchecked
ChunksExactMut	next, nth, next_back, nth_back
RChunks	next, next_back, __iterator_get_unchecked
RChunksMut	next, nth, last, next_back, nth_back, __iterator_get_unchecked
RChunksExact	new, __iterator_get_unchecked
RChunksExactMut	next, nth, next_back, nth_back, __iterator_get_unchecked
ArrayWindows	next, next_back (N=1,2,4), nth, nth_back (N=2,4)
Windows	__iterator_get_unchecked

Verification approach

• Symbolic inputs via kani::any() and kani::slice::any_slice_of_array
• Arbitrary subslice construction with nondeterministic bounds
• Concrete closures for predicate-based iterators (Split)
• Monomorphized const generics for ArrayWindows (N=1,2,4)
• Iter safety invariant checked via iter.is_safe() assertions

Test plan

• Kani CI: All 52 harnesses pass via kani verify-std
• No changes to runtime logic
• Existing Iter harnesses (18) continue to pass