Verify safety of slice functions (Challenge 17)

[jrey8343]

Summary

Adds 37 Kani verification harnesses proving the safety of all unsafe operations in library/core/src/slice/mod.rs, covering all 37 functions listed in Challenge 17. Also adds #[requires] safety contracts to 5 unsafe functions (the remaining 2 unsafe functions, align_to/align_to_mut, had pre-existing contracts and harnesses).

Unsafe function contracts added

Function	Contract
swap_unchecked	#[requires(a < self.len() && b < self.len())]
as_chunks_unchecked	#[requires(N != 0 && self.len() % N == 0)]
as_chunks_unchecked_mut	#[requires(N != 0 && self.len() % N == 0)]
split_at_unchecked	#[requires(mid <= self.len())]
split_at_mut_unchecked	#[requires(mid <= self.len())]

Functions verified

Function	Harness	Unsafe operation
first_chunk	check_first_chunk	Length check + pointer cast
first_chunk_mut	check_first_chunk_mut	Length check + pointer cast (mut)
split_first_chunk	check_split_first_chunk	split_at_unchecked
split_first_chunk_mut	check_split_first_chunk_mut	split_at_unchecked (mut)
split_last_chunk	check_split_last_chunk	split_at_unchecked
split_last_chunk_mut	check_split_last_chunk_mut	split_at_unchecked (mut)
last_chunk	check_last_chunk	Length check + pointer cast
last_chunk_mut	check_last_chunk_mut	Length check + pointer cast (mut)
as_chunks	check_as_chunks	as_chunks_unchecked + split_at_unchecked
as_chunks_mut	check_as_chunks_mut	as_chunks_unchecked_mut + split_at_mut_unchecked
as_rchunks	check_as_rchunks	as_chunks_unchecked + split_at_unchecked
as_rchunks_mut	check_as_rchunks_mut	as_chunks_unchecked_mut + split_at_mut_unchecked
as_flattened	check_as_flattened	from_raw_parts with unchecked_mul
as_flattened_mut	check_as_flattened_mut	from_raw_parts_mut with unchecked_mul
swap_unchecked	check_swap_unchecked	get_unchecked + ptr::swap
as_chunks_unchecked	check_as_chunks_unchecked	from_raw_parts pointer cast
as_chunks_unchecked_mut	check_as_chunks_unchecked_mut	from_raw_parts_mut pointer cast
split_at_unchecked	check_split_at_unchecked	get_unchecked + get_unchecked_mut
split_at_mut_unchecked	check_split_at_mut_unchecked	split_at_mut_unchecked
get_unchecked (usize)	check_get_unchecked_usize	SliceIndex::get_unchecked
get_unchecked_mut (usize)	check_get_unchecked_mut_usize	SliceIndex::get_unchecked (mut)
get_unchecked (Range)	check_get_unchecked_range	SliceIndex::get_unchecked
get_unchecked_mut (Range)	check_get_unchecked_mut_range	SliceIndex::get_unchecked (mut)
get_disjoint_unchecked_mut	check_get_disjoint_unchecked_mut	Multiple get_unchecked_mut calls
split_at_checked	check_split_at_checked	split_at_unchecked
split_at_mut_checked	check_split_at_mut_checked	split_at_mut_unchecked
copy_from_slice	check_copy_from_slice	ptr::copy_nonoverlapping
swap_with_slice	check_swap_with_slice	ptr::swap_nonoverlapping
copy_within	check_copy_within	ptr::copy
get_disjoint_mut	check_get_disjoint_mut	get_disjoint_unchecked_mut
get_disjoint_check_valid	check_get_disjoint_check_valid	Index bounds validation
rotate_left	check_rotate_left	rotate::ptr_rotate
rotate_right	check_rotate_right	rotate::ptr_rotate
binary_search_by	check_binary_search_by	get_unchecked in binary search loop
partition_dedup_by	check_partition_dedup_by	ptr::read, ptr::copy_nonoverlapping, ptr::write
as_simd	check_as_simd	align_to + from_raw_parts
as_simd_mut	check_as_simd_mut	align_to_mut + from_raw_parts_mut
reverse	pre-existing check_reverse	ptr::read, ptr::copy_nonoverlapping, ptr::write
align_to	pre-existing harnesses	Pointer alignment cast
align_to_mut	pre-existing harnesses	Pointer alignment cast (mut)

Verification approach

• Chunk/split functions: Symbolic-length slices via kani::slice::any_slice_of_array with small backing arrays (4-8 elements), proving all pointer casts and unchecked splits are in bounds.
• Unsafe contracts: #[kani::proof_for_contract] harnesses for as_chunks_unchecked, as_chunks_unchecked_mut, split_at_unchecked, split_at_mut_unchecked. Plain #[kani::proof] for swap_unchecked (CBMC assigns clause interference with memmove builtins).
• get_unchecked: Verified with both usize and Range<usize> index types, with symbolic indices constrained to valid bounds.
• rotate_left/right: 5-element concrete array with symbolic rotation amount, using ptr_rotate stub (CBMC-intractable BufType = [usize; 32] stack buffer).
• swap_with_slice: Symbolic-length slices with swap_nonoverlapping stub (CBMC-intractable byte-level swapping with symbolic lengths).
• binary_search_by / partition_dedup_by: 7-element sorted arrays with #[kani::unwind(8)].
• as_simd/as_simd_mut: Concrete f32 arrays verifying SIMD alignment and casting.

All 37 new harnesses verified locally (45 total including 8 pre-existing harnesses).

Test plan

• All 37 new harnesses pass with kani verify-std using -Z loop-contracts --cbmc-args --object-bits 12
• Pre-existing 8 harnesses remain passing
• Code formatted with rustfmt