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)

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).