Challenge 17: Verify safety of Slice functions

[Samuelsills]

Summary

Add Kani proof harnesses verifying all 37 slice functions specified in Challenge #17:

• 10 unsafe functions: get_unchecked, get_unchecked_mut, swap_unchecked, as_chunks_unchecked, as_chunks_unchecked_mut, split_at_unchecked, split_at_mut_unchecked, align_to, align_to_mut, get_disjoint_unchecked_mut
• 27 safe abstractions: first_chunk, first_chunk_mut, split_first_chunk, split_first_chunk_mut, split_last_chunk, split_last_chunk_mut, last_chunk, last_chunk_mut, reverse, as_chunks, as_chunks_mut, as_rchunks, split_at_checked, split_at_mut_checked, binary_search_by, partition_dedup_by, rotate_left, rotate_right, copy_from_slice, copy_within, swap_with_slice, as_simd, as_simd_mut, get_disjoint_mut, get_disjoint_check_valid, as_flattened, as_flattened_mut

All harnesses verified locally with Kani.

Resolves #281

[Samuelsills]

Verification Coverage Report

Unsafe Functions (10/10 ✅)

get_unchecked, get_unchecked_mut, swap_unchecked, as_chunks_unchecked, as_chunks_unchecked_mut, split_at_unchecked, split_at_mut_unchecked, align_to, align_to_mut, get_disjoint_unchecked_mut

Safe Abstractions (27/27 ✅)

first_chunk, first_chunk_mut, split_first_chunk, split_first_chunk_mut, split_last_chunk, split_last_chunk_mut, last_chunk, last_chunk_mut, reverse, as_chunks, as_chunks_mut, as_rchunks, split_at_checked, split_at_mut_checked, binary_search_by, partition_dedup_by, rotate_left, rotate_right, copy_from_slice, copy_within, swap_with_slice, as_simd, as_simd_mut, get_disjoint_mut, get_disjoint_check_valid, as_flattened, as_flattened_mut

Total: 37/37 functions verified

UBs Checked (automatic via Kani/CBMC)

• ✅ Accessing dangling or misaligned pointers
• ✅ Reading from uninitialized memory
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• align_to/align_to_mut verified via pre-existing proof_for_contract harnesses (64 macro-expanded variants each)
• 37 proof harnesses covering all spec functions

[Copilot]

Pull request overview

This PR extends core::slice’s existing #[cfg(kani)] mod verify with additional Kani proof harnesses intended to model-check the safety/correctness of the slice APIs listed in Challenge #17 (resolving #281).

Changes:

• Add Kani proof harnesses for a wide set of slice APIs (unchecked accessors, chunking/splitting helpers, copy/swap/rotate, SIMD views, and disjoint-borrow helpers).
• Introduce a small fixed-length model (SLICE_LEN) to keep harness state spaces bounded while exercising these APIs.

[Copilot]

check_split_at_mut_checked creates s: &mut [i32] = &mut arr; and then, in the else branch, creates a second mutable borrow s2: &mut [i32] = &mut arr;. This pattern typically fails the borrow checker because arr is already mutably borrowed by s for the whole if statement. Use the existing s in both branches, or move the &mut arr borrow into each branch so there is never more than one &mut borrow of arr in scope at a time.

Suggested change

	let s2: &mut [i32] = &mut arr;
	assert!(s2.split_at_mut_checked(mid).is_none());
	assert!(s.split_at_mut_checked(mid).is_none());

[Copilot]

The harness for get_disjoint_check_valid only explores in-bounds indices (a/b are constrained to < SLICE_LEN), so it can never exercise/verify the IndexOutOfBounds error path that this helper is responsible for. Consider allowing a/b to range over arbitrary usize values and asserting Err(IndexOutOfBounds) when either is out of bounds, in addition to the overlapping-indices case.

Suggested change

	let a: usize = kani::any_where(|&i: &usize| i < SLICE_LEN);
	let b: usize = kani::any_where(|&i: &usize| i < SLICE_LEN);
	let indices = [a, b];
	let result = get_disjoint_check_valid(&indices, SLICE_LEN);
	if a == b {
	assert!(result.is_err());
	} else {
	let a: usize = kani::any();
	let b: usize = kani::any();
	let indices = [a, b];
	let result = get_disjoint_check_valid(&indices, SLICE_LEN);
	if a >= SLICE_LEN || b >= SLICE_LEN {
	// At least one index is out of bounds; the check must fail.
	assert!(result.is_err());
	} else if a == b {
	// In-bounds but overlapping indices must also be rejected.
	assert!(result.is_err());
	} else {
	// In-bounds and distinct indices should be accepted.

[Copilot]

check_get_disjoint_mut assumes a != b and both indices are in-bounds, which only verifies the success path. Since get_disjoint_mut is a safe API whose safety relies on returning Err (not panicking/UB) for out-of-bounds or overlapping indices, it would be stronger to remove the a != b assumption and assert that the result matches the expected GetDisjointMutError for the invalid cases as well.

Suggested change

	let a: usize = kani::any_where(|&i: &usize| i < SLICE_LEN);
	let b: usize = kani::any_where(|&i: &usize| i < SLICE_LEN);
	kani::assume(a != b);
	let result = arr.get_disjoint_mut([a, b]);
	assert!(result.is_ok());
	let [ra, rb] = result.unwrap();
	*ra = 1;
	*rb = 2;
	assert_eq!(arr[a], 1);
	assert_eq!(arr[b], 2);
	let a: usize = kani::any();
	let b: usize = kani::any();
	let expected_ok = a < SLICE_LEN && b < SLICE_LEN && a != b;
	let result = arr.get_disjoint_mut([a, b]);
	if expected_ok {
	assert!(result.is_ok());
	let [ra, rb] = result.unwrap();
	*ra = 1;
	*rb = 2;
	assert_eq!(arr[a], 1);
	assert_eq!(arr[b], 2);
	} else {
	assert!(result.is_err());
	}