Verify safety of slice functions with Kani (Challenge 17)

Add contracts and proof harnesses for 34 slice functions covering:
- Chunk operations (first_chunk, last_chunk, as_chunks, as_rchunks, as_flattened)
- Unsafe accessors (get_unchecked, swap_unchecked, split_at_unchecked)
- Safe wrappers with pointer ops (copy_from_slice, swap_with_slice, copy_within)
- Complex functions (reverse, rotate_left/right, binary_search_by, partition_dedup_by, as_simd)
- Disjoint mutable access (get_disjoint_mut, get_disjoint_unchecked_mut)

Contracts added to: swap_unchecked, as_chunks_unchecked, as_chunks_unchecked_mut,
split_at_unchecked, split_at_mut_unchecked.

All 37 new harnesses verified with Kani 0.65.0.

Author: jrey8343