Verify safety of slice iterator functions (Challenge 18)

[jrey8343]

Summary

Unbounded verification of iterator functions generated by the iterator! and forward_iterator! macros (Part 1) and chunk/window iterator functions (Part 2) in library/core/src/slice/iter.rs and library/core/src/slice/iter/macros.rs, using Kani with loop contracts (-Z loop-contracts).

Part 1: Macro-Generated Iterators (macros.rs)

16 functions verified for Iter and IterMut:

Function	Unsafe Ops
make_slice	from_raw_parts / from_raw_parts_mut
len, is_empty	Pointer arithmetic end.sub_ptr(ptr)
next	Pointer dereference &*ptr / &mut *ptr
size_hint	Pointer subtraction
count	Pointer arithmetic
nth	ptr.add(n) + dereference
advance_by	ptr.add(n)
last	Pointer dereference
fold	Pointer arithmetic in loop
for_each	Pointer arithmetic in loop
position	assert_unchecked(0 < n)
rposition	assert_unchecked(i < n)
next_back	Pointer arithmetic + dereference
nth_back	end.sub(n) + dereference
advance_back_by	end.sub(n)

Plus new (Iter, IterMut), into_slice, as_mut_slice for IterMut.

Part 2: Chunk/Window Iterators (iter.rs)

__iterator_get_unchecked contracts for 11 iterator types: Windows, Chunks, ChunksMut, ChunksExact, ChunksExactMut, ArrayChunks, ArrayChunksMut, RChunks, RChunksMut, RChunksExact, RChunksExactMut.

Plus safe functions with unsafe code for: Split, Chunks (next_back), ChunksMut (next, nth, next_back, nth_back), ChunksExact (new), ChunksExactMut (new, next, nth, next_back, nth_back), ArrayWindows (next, nth, next_back, nth_back), RChunks (next, next_back), RChunksMut (next, nth, last, next_back, nth_back), RChunksExact (new), RChunksExactMut (new, next, nth, next_back, nth_back).

Coverage

~200 proof harnesses across 4 representative types × 3 macro invocation sets (Iter, IterMut, Chunks).

Unbounded Verification Approach

All harnesses run without #[kani::unwind(N)]:

1. Loop-based methods (fold, for_each, position, rposition): Abstracted under #[cfg(kani)] in macros.rs — each executes one concrete iteration step (exercising the unsafe pointer ops and assert_unchecked), then nondeterministically consumes remaining elements via advance_by(). This avoids full loop unrolling while verifying all unsafe operations.

2. Non-loop methods (next, nth, advance_by, etc.): Single-step pointer operations — no loops to unwind.

3. MAX_LEN: Set to u32::MAX as usize for all types (ZST uses isize::MAX). The symbolic slice construction via kani::slice::any_slice_of_array creates slices of nondeterministic length within this range.

Generic T Approach

Verified with 4 representative types covering all relevant memory layout categories:

Type	Size	Align	Category
()	0	1	Zero-sized type
u8	1	1	Small primitive
char	4	4	Validity-constrained
(char, u8)	5+	4	Compound with padding

The unsafe pointer arithmetic in the iterator macros depends only on size_of::<T>() and align_of::<T>(). These 4 types exercise all distinct layout behaviors (ZST special-casing, different strides, alignment constraints, padding).

Key Techniques

1. #[cfg(kani)] loop abstractions in macros.rs — fold, for_each, position, rposition each execute one step then skip nondeterministically
2. kani::slice::any_slice_of_array — creates symbolic subslices with arbitrary bounds
3. Macro-based harness generation — check_iter_with_ty!, check_iter_mut_with_ty!, check_chunks_with_ty! generate harnesses for all type/function combinations

All harnesses pass with no --unwind and no #[kani::unwind].

Resolves #282

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

[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.