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

🤖 Generated with Claude Code

[jrey8343]

Note on "no monomorphization" requirement: We've asked for clarification on the tracking issue about whether Kani's representative-types approach (4 types covering all layout categories: ZST, small, validity-constrained, compound) satisfies this requirement. Kani fundamentally monomorphizes, so a VeriFast-based alternative is also being explored. See the tracking issue for details.

[jrey8343]

Update on "generic T" requirement:

Same status as #559 — awaiting committee guidance on #281 re: representative types, and pursuing VeriFast &[T] support upstream (verifast/verifast#1001) for full generic-T coverage via separation logic.

Converting to draft until the path forward is clear.