Verify the safety of slice functions (challenge #17)

[MavenRain]

Challenge 17: Verify the safety of slice functions

Resolves the verification targets in doc/src/challenges/0017-slice.md (tracking #281).
This adds Kani harnesses for all 37 functions in the challenge: the 10 unsafe
functions (with safety contracts) and the 27 safe abstractions (proven UB-free).

Unsafe functions (contracts + proof_for_contract)

function	precondition	notes
get_unchecked / get_unchecked_mut	index in bounds	see "index genericity" below
swap_unchecked	a < len && b < len	#[requires] + kani::modifies(self)
split_at_unchecked / split_at_mut_unchecked	mid <= len	#[requires]
as_chunks_unchecked / as_chunks_unchecked_mut	N != 0 && len % N == 0	#[requires], per concrete <[T]>::…::<N>
align_to / align_to_mut	(pre-existing on main)	unchanged
get_disjoint_unchecked_mut	indices in bounds + pairwise disjoint	see "index genericity"

Safe abstractions (proven free of UB)

first_chunk(_mut), last_chunk(_mut), split_first_chunk(_mut), split_last_chunk(_mut),
split_at_checked, split_at_mut_checked, as_chunks, as_chunks_mut, as_rchunks,
as_flattened, as_flattened_mut, as_simd, as_simd_mut, binary_search_by,
get_disjoint_mut, get_disjoint_check_valid, copy_from_slice, copy_within,
swap_with_slice, partition_dedup_by, rotate_left, rotate_right (and reverse,
pre-existing on main).

Approach

• Harnesses live in the existing #[cfg(kani)] mod verify at the end of
  library/core/src/slice/mod.rs, following the established align_to pattern.
• Generic functions are checked at concrete monomorphizations:
  #[kani::proof_for_contract(<[T]>::method)] (incl. const-generic turbofish
  <[T]>::as_chunks_unchecked::<N>), spread over representative element types
  ((), u8, u64, char, …) and chunk sizes — source-generic, proof-concrete.
• Slices are built with the symbolic-length kani::slice::any_slice_of_array(_mut)
  helper (the same "unbounded" encoding align_to uses).
• Looping abstractions (binary_search_by, rotate_*, copy_*, swap_with_slice,
  partition_dedup_by) carry an explicit #[kani::unwind(K)] — a verified
  unwinding assertion, not an assumption.

Honest caveats (please review)

1. Bounded backing arrays. As with the existing align_to harnesses, the symbolic
   slice length ranges over [0, ARR_SIZE] for a fixed ARR_SIZE. The per-index/-element
   safety obligation is structurally identical at every position, so a modest bound
   exercises it, but coverage is bounded rather than literally unbounded.
2. Index genericity (get_unchecked, get_unchecked_mut, get_disjoint_*). The
   safety precondition is index-type-specific (idx < len for usize; range bounds for
   Range) and cannot be expressed as one #[requires] over the generic index I
   (a contract closure only borrows its args, and SliceIndex exposes no generic
   in-bounds predicate). These are proven with plain #[kani::proof] at concrete index
   types, with the documented caller obligation established by kani::assume. Same property
   the contract would express; happy to adjust if you'd prefer a different encoding.
3. rotate_left / rotate_right are per-config, not symbolic-length. A symbolic
   rotation amount makes ptr_rotate perform symbolic-size memcpys at a symbolic split
   point and explore its block-swap/juggling paths; CBMC exceeded a 6 GB budget (and kept
   climbing) even at length 4 on the dev machine. They are instead verified over
   representative concrete (length, amount) configurations with symbolic element values
   (a single concrete ptr_rotate path). A higher-memory environment could attempt the
   fully symbolic version.
4. swap_unchecked omits the ZST instantiation. kani::modifies(self) over a
   zero-size slice region trips a CBMC contracts-library limitation (car_set_insert);
   swapping ZSTs moves zero bytes, so it is trivially safe. The non-ZST instantiations
   exercise the actual ptr::swap writes.

Tooling / disclosure

Verified with the repo's pinned Kani (commit 415ca50, nightly-2025-10-09) via
verify-std. Authored with AI assistance (Claude); all proofs were run and confirmed
to pass locally (sequential CBMC).

[MavenRain]

Status update for reviewers: this PR is green on every check and mergeable
against current main.

It verifies all 37 functions in challenge #17: the 10 unsafe functions with
safety contracts and the 27 safe abstractions proven free of UB. The four honest
caveats are written up in the description (bounded backing arrays, index
genericity for get_unchecked / get_disjoint_*, per-config rotate_left /
rotate_right, and the ZST omission for swap_unchecked), each with its
reasoning and soundness argument. Those are the points most likely to want a
reviewer's judgment, and I am happy to adjust any of them, including attempting
fully symbolic rotation in a higher-memory environment if that matters for
acceptance.

The claim is on the tracking issue (#281) and the challenge is otherwise quiet.
Thanks for taking a look whenever you have a chance.