[v3risec]

Summary

This PR adds safety contracts and Kani verification harnesses for Challenge 18: slice iterator functions.

The changes:

• extend the existing #[cfg(kani)] mod verify in slice/iter.rs;
• add contracts and contract harnesses for unchecked iterator access;
• add shared symbolic-slice helpers and macro-generated harnesses for iterator, splitting, window, and chunk families;
• check return values, pointer identity, remaining lengths, and iterator state, with kani::cover checks for relevant paths;
• add Kani-only loop annotations and independently proved arithmetic and pointer helpers.

Normal-build iterator implementations are unchanged. Unrelated formatting changes have been removed.

Verification progress

The following results have been recorded locally:

• Four native Kani harness successes for u8 IterMut construction, slice views, and retained mutable elements.
• 8/8 local access-safety proofs for the next, nth, next_back, and nth_back operations of ChunksExactMut and RChunksExactMut.
• 6/8 complete functional harness proofs for those two iterator families: all four ChunksExactMut operations, plus RChunksExactMut::next and RChunksExactMut::next_back.

The six functional proofs use complete property partitions of frozen models, including the original manual cover checks. They are not reported as native, single-run Kani successes.

RChunksExactMut::nth and RChunksExactMut::nth_back remain incomplete as full functional harnesses. Other type and method combinations also require further verification.

This PR does not yet claim completion of Challenge 18.

Towards #282

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