Add Kani harnesses for Challenge 18: slice iter functions

[MavenRain]

Solution to Challenge 18: verify the safety of slice iter functions.

Part 1

• All 16 functions from the iterator! macro are proved for IterMut (make_slice, len, is_empty, next, size_hint, count, nth, advance_by, last, fold, for_each, position, rposition, next_back, nth_back, advance_back_by). Iter coverage already exists on main and stays green.
• next and size_hint are proved for SplitN, SplitNMut, RSplitN, and RSplitNMut through the forward_iterator! path.

Part 2

• The current snapshot of slice/iter.rs contains 9 __iterator_get_unchecked impls: Windows, Chunks, ChunksMut, ChunksExact, ChunksExactMut, RChunks, RChunksMut, RChunksExact, RChunksExactMut. ArrayChunks and ArrayChunksMut no longer exist in this file.
• Each of the 9 gets a safety contract (#[requires]/#[ensures]) on a private contracted inherent method. The __iterator_get_unchecked trait method delegates to it. Each contract is proved with #[kani::proof_for_contract]. This pattern sidesteps the known interaction between proof_for_contract and generic trait methods.
• All safe functions with unsafe bodies from the second table have harnesses: the constructors (Iter::new, IterMut::new, ChunksExact::new, ChunksExactMut::new, RChunksExact::new, RChunksExactMut::new), IterMut::{into_slice, as_mut_slice}, the Split family, ArrayWindows, and the chunk-family next/nth/last/next_back/nth_back methods.

Approach and disclosures

• Generic code is instantiated over representative types: () (ZST), u8, char (validity invariant), and (char, u8) (padding). Kani cannot emit one proof for all T; this per-type spread is the same pattern the merged solutions for challenges 16 and 17 use.
• Element values are symbolic in every harness. Backing lengths are symbolic up to isize::MAX for () and u32::MAX for u8; char and (char, u8) use smaller symbolic bounds to keep solver time practical.
• Looping harnesses (fold, for_each, position, rposition, last, and the split families) use #[kani::unwind] bounds. Kani verifies the unwinding assertion, so a bound that is too small fails loudly.
• Verified locally at the pinned Kani commit d4df833c (toolchain nightly-2025-11-25): 385 of 385 harnesses successful, 0 failures.
• AI assistance (Claude) was used to write the harnesses. All proofs were checked locally with the pinned Kani version.

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.