Verify safety of slice functions (Challenge 17)

[kasimte]

Towards #281.

Kani harnesses and safety-precondition contracts for Challenge 17: Verify the safety of slice functions — the 10 unsafe functions (contracts + no-UB) and the 27 safe functions (no-UB) from core::slice. This adds 43 harnesses to slice::verify; align_to/align_to_mut (unsafe) and reverse (safe) already have harnesses there and are unchanged. Each harness runs the real shipped body — no #[cfg(kani)] rewrite — and every assume-bearing harness carries a satisfied kani::cover (32 total). All pass via scripts/run-kani.sh.

Unbounded length and generic T are not literally met. This is left as a committee question open across the sentence-pair challenges, and is disclosed under Limitations. Most slices are verified over a symbolic length bounded by a concrete backing array (kani::slice::any_slice_of_array); get_disjoint_check_valid, which takes a raw length, is verified over a fully symbolic length; partition_dedup_by (fixed length 4) and the rotate_* dispatch harnesses (lengths fixed to select an algorithm) are verified over fixed lengths. The four loop-bearing functions (binary_search_by, partition_dedup_by, swap_with_slice, rotate_*) additionally carry kani::unwind bounds, each for the reason noted with the function below.

Success criteria

Criterion	Status
10 unsafe functions — safety-precondition contracts + no-UB	Done, with a disclosed residual: 5 via #[requires] + proof_for_contract; the get_unchecked trio via a mirrored kani::assume (proof_for_contract can't resolve them at the pinned Kani — see Upstream Kani contributions); align_to/align_to_mut pre-existing.
27 safe functions — no-UB	Done.
Absence of the listed UBs	Done — Kani checks them on every harness.
Unbounded (arbitrary length)	Not literally met — symbolic length bounded by the backing array (loop-free functions are length-agnostic); committee question, see Limitations.
Generic T (no monomorphization)	Not literally met — representative types (Kani monomorphizes); committee question, see Limitations.

What the harnesses check

• Real bodies. Safety-precondition contracts on the unsafe functions (proof_for_contract where the trait impl resolves); no-UB harnesses on the safe functions. No #[cfg(kani)] body rewrites.
• Documented panics as should_panic pairs (4: swap_with_slice/copy_from_slice length mismatch, copy_within/rotate_left out-of-range).
• rotate dispatch. ptr_rotate selects one of three algorithms by element size; the memmove and gcd algorithms are verified (dispatch confirmed from the run trace). The swap algorithm is reached only for very large slices (min(left, right) > 256 / size_of::<T>, i.e. hundreds of elements) — intractable at the CI object budget, so it is disclosed rather than verified.
• Non-vacuity. Every assume-bearing harness carries a satisfied kani::cover (32 total).

Per-function coverage (click to expand)

Unsafe (10):

Function	Harness	Form
get_unchecked	check_get_unchecked_usize	assume-mirror
get_unchecked_mut	check_get_unchecked_mut_usize	assume-mirror
get_disjoint_unchecked_mut	check_get_disjoint_unchecked_mut_usize_2	assume-mirror
swap_unchecked	check_swap_unchecked_u8	#[requires] + proof_for_contract
as_chunks_unchecked	check_as_chunks_unchecked_u8_4	#[requires] + proof_for_contract
as_chunks_unchecked_mut	check_as_chunks_unchecked_mut_u8_4	#[requires] + proof_for_contract
split_at_unchecked	check_split_at_unchecked_u8	#[requires] + proof_for_contract
split_at_mut_unchecked	check_split_at_mut_unchecked_u8	#[requires] + proof_for_contract
align_to	macro-generated proof_for_contract matrix (src×dst types)	pre-existing
align_to_mut	macro-generated proof_for_contract matrix (src×dst types)	pre-existing

Safe (27):

Function	Harness
first_chunk / first_chunk_mut	check_first_chunk_3 / check_first_chunk_mut_3
split_first_chunk / split_first_chunk_mut	check_split_first_chunk_3 / check_split_first_chunk_mut_3
split_last_chunk / split_last_chunk_mut	check_split_last_chunk_3 / check_split_last_chunk_mut_3
last_chunk / last_chunk_mut	check_last_chunk_3 / check_last_chunk_mut_3
as_chunks / as_chunks_mut	check_as_chunks_3, check_as_chunks_4 / check_as_chunks_mut_3
as_rchunks	check_as_rchunks_3, check_as_rchunks_4
split_at_checked / split_at_mut_checked	check_split_at_checked / check_split_at_mut_checked
as_flattened / as_flattened_mut	check_as_flattened / check_as_flattened_mut
copy_from_slice	check_copy_from_slice (+ check_copy_from_slice_len_mismatch)
copy_within	check_copy_within (+ check_copy_within_oob)
swap_with_slice	check_swap_with_slice (+ check_swap_with_slice_len_mismatch)
as_simd / as_simd_mut	check_as_simd_i32 / check_as_simd_mut_i32
get_disjoint_mut	check_get_disjoint_mut_usize_2
get_disjoint_check_valid	check_get_disjoint_check_valid_usize_2 (fully symbolic length)
binary_search_by	check_binary_search_by (bounded)
partition_dedup_by	check_partition_dedup_by_spike (fixed length 4)
rotate_left	check_rotate_memmove_u8, check_rotate_gcd_big_t, check_rotate_zst, check_rotate_noop_zero (+ check_rotate_left_oob)
rotate_right	check_rotate_right_memmove_u8
reverse	check_reverse (pre-existing)

Upstream Kani contributions

The get_unchecked trio is verified through a mirrored kani::assume because proof_for_contract can't resolve generic trait-impl methods at the pinned Kani. We fixed that upstream in model-checking/kani#4865 (merged; not yet in this pin) — once a pin bump includes it, those functions can return to proof_for_contract. The bounded-binary_search_by limit below is filed as model-checking/kani#4911, which now records the measured root cause; the bound can drop once upstream fixes for it land in a pin bump.

How to verify

scripts/run-kani.sh -Z unstable-options ./library \
  -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi \
  -Z loop-contracts -Z quantifiers -Z stubbing --cbmc-args --object-bits 12

Expected: every harness in slice::verify passes, with each cover satisfied.

Limitations (disclosed)

• Unbounded (arbitrary length). A real slice is verified over a symbolic length bounded by its concrete backing array (any_slice_of_array); a slice of unbounded symbolic length is not constructible in Kani (a real slice needs backing memory). The loop-free functions are length-agnostic, so the bounded proof is representative; get_disjoint_check_valid (taking a raw length) is verified over a fully symbolic length. This is the arbitrary-length half of the sentence-pair committee question.
• Loop-bearing functions: additionally bounded via kani::unwind, each for a specific reason noted in-code:
  • binary_search_by — get_unchecked's precondition is not discharged when the comparator closure receives the element by reference (Loop contract: get_unchecked precondition not discharged when the slice element is passed into a closure kani#4911).
  • partition_dedup_by — an explicit loop_modifies clause cannot name the loop body's compiler-generated temporaries, so no valid modifies set can be formed for a loop-invariant proof.
  • swap_with_slice — the element copy runs through swap_nonoverlapping's internal chunked loop, a shared function that carries no loop contract, so it requires an unwind bound.
  • rotate_left/rotate_right — the memmove and gcd algorithms are verified; the swap algorithm needs hundreds of elements and is intractable at the CI object budget (see the rotate dispatch note above).
• Generic T: representative types. Kani operates on concrete GOTO programs, so a single proof generic over T is not expressible. The unsafe operations depend on size_of/align_of/drop glue, not type identity; the representative types cover those axes. This is the generic-T half of the sentence-pair committee question.
• Every changed line is additive (+374 / −0, one file); no runtime logic is modified.

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