[kasimte]

Towards #281. Verifies the safety of core::slice functions with Kani (Challenge 17).

Harnesses in slice::verify for all 10 unsafe and all 27 safe functions; align_to, align_to_mut, reverse pre-existing, unchanged. Each runs the real shipped body; additive, no #[cfg(kani)] rewrite. All pass via scripts/run-kani.sh at Kani 6ce55b9 / CBMC 6.11, with 33 kani::cover reachability witnesses (all satisfied) and 4 should_panic pairs.

Spec requirement	Status
10 unsafe fns — safety contracts + no UB	all 10, per method — proof_for_contract, or a mirrored kani::assume for the get_unchecked trio (Contracts below)
27 safe fns — no UB	all 27 — no-UB over symbolic-length slices
Listed UBs absent	dangling/misaligned checked by Kani's defaults, invalid-value where raw bytes become typed; uninitialized-read (opt-in, not in run-kani.sh) and mutating-immutable-bytes (no Kani check class) are repo-wide gaps
Unbounded length	partial — symbolic length over a concrete backing array; four loop-bearing fns bounded (below)
Generic T	representative, not parametric; open committee question (#734)

Contracts. Five unsafe fns (swap_unchecked, split_at_unchecked/_mut_unchecked, as_chunks_unchecked/_mut) carry #[requires] + proof_for_contract. The get_unchecked trio instead assume-mirrors the index < len precondition: get_unchecked dispatches through the generic SliceIndex trait, whose impls carry no #[requires] contract — only assert_unsafe_precondition!, with an index-type-specific bound — so there is nothing for proof_for_contract to target; the mirror states the concrete precondition and proves the same no-UB property.

Bounded functions. Three take a kani::unwind at a tool wall instead of an unbounded loop contract: binary_search_by (get_unchecked's precondition is not discharged when the comparator takes the element by reference); partition_dedup_by (an explicit loop_modifies cannot name the loop's compiler-generated temporaries); and swap_with_slice (the copy runs through swap_nonoverlapping's shared chunked loop). A loop contract is size-independent, so each of these drops to unbounded once its upstream fix reaches this pin. rotate_left/rotate_right verify all three algorithm arms (memmove, gcd, swap); the memmove arm is loop-free, the gcd and swap arms run under routine finite unwinds.

Generic T. Kani operates on concrete GOTO programs, so a single proof generic over T is not expressible; it is the open committee question (#734). The unsafe operations depend on size_of, align_of, and drop glue, not type identity. Where a verified function branches on type size or alignment, the harnesses reach every arm: align_to/align_to_mut over the proof_for_contract type matrix (align_of 1–16 and the ZST arm), and ptr_rotate's size_of-gated memmove/gcd/swap dispatch.

Upstream Kani. We filed the binary_search_by loop wall kani#4911 and its fix kani#4957 (open); it drops that bound once it lands.

Verify with scripts/run-kani.sh (the standard -Z flags, --object-bits 12).

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

[feliperodri]

Challenge 17 requires: "The verification must be unbounded---it must hold for slices of arbitrary length." That requirement is final. A Kani solution will only be accepted if it is unbounded in the input size for every required function. This PR still verifies at least part of the challenge with bounded harnesses (kani::unwind bounds and/or fixed-size inputs), so I'm requesting changes until every required function is verified without a bound on the input size.