Challenge 17: Verify slice safety with Kani

[v3risec]

Summary

This PR adds Kani-based safety verification for the slice APIs listed in Challenge 17.

The changes provide:

• safety contracts for all 10 unsafe functions required by the challenge
• direct harness coverage for all 27 required safe abstractions
• contract predicates and harnesses for every current SliceIndex<[T]> implementation
• coverage for all five GetDisjointMutIndex implementations
• loop contracts for reverse, binary_search_by, partition_dedup_by, and the pointer-swap loops reached by slice operations
• representative concrete element types covering signed and unsigned integer widths, restricted-validity scalar types, ZSTs, and aggregate layouts

Verification-only helpers and harnesses are gated by cfg(kani). The standard library runtime algorithms are not replaced by Kani-specific implementations.

Challenge Coverage

Requirement	Coverage	Notes
Unsafe functions	10 / 10	Safety contracts and contract proof harnesses
Safe abstractions	27 / 27	Direct harness coverage for every listed function

The existing align_to, align_to_mut, and reverse verification is retained and included in the coverage above.

Verification Approach

Contracts and frame conditions

Semantic contract annotations follow the repository-wide safety contract style: requires expresses documented caller obligations, ensures captures the existing align_to{,_mut} postconditions, and safety::loop_invariant states the safety relationships preserved by loops. Kani-specific modifies and loop_modifies annotations are used only for frame conditions, making explicit which slices, pointer regions, and loop-local state may change. This keeps semantic safety conditions separate from verifier-specific memory framing while retaining the real standard-library implementations.

Harness and type coverage

Unsafe functions are connected directly to their contracts with #[kani::proof_for_contract], so Kani verifies their real bodies under the declared preconditions and checks their postconditions. Safe abstractions use #[kani::proof] harnesses, including dedicated panic-path harnesses where applicable. The harness matrix covers i8 through i128, u8 through u128, bool, char, (), and [u8; 4], exercising different widths, alignments, validity constraints, ZST behavior, and aggregate layouts. Index-generic proofs cover every current SliceIndex<[T]> implementation, including usize, IndexRange, legacy and new range types, bound pairs, Clamp, Last, and exhausted legacy RangeInclusive states. The disjoint-index proofs additionally cover all five current GetDisjointMutIndex implementations.

Unsafe contracts

The contracts express the documented caller obligations for:

• get_unchecked and get_unchecked_mut
• swap_unchecked
• as_chunks_unchecked and as_chunks_unchecked_mut
• split_at_unchecked and split_at_mut_unchecked
• align_to and align_to_mut
• get_disjoint_unchecked_mut

get_unchecked and get_unchecked_mut use a Kani-only kani_in_bounds predicate on the sealed SliceIndex trait. Every current implementation provides its exact bounds condition, including legacy and new range APIs, bound pairs, Clamp, Last, and exhausted legacy RangeInclusive states.

get_disjoint_unchecked_mut uses the same complete bounds-and-overlap check as the safe API. Its contract and safe harnesses cover usize, ops::{Range, RangeInclusive}, and range::{Range, RangeInclusive}.

Loop contracts

The loop invariants preserve the index and pointer relationships required by unchecked accesses in reverse, binary_search_by, and partition_dedup_by.

The original loops remain in place. Kani-only local declarations make per-iteration temporary values available to loop frame conditions without replacing the algorithms or their control flow.

Rotation

rotate_left and rotate_right call the real ptr_rotate implementation.
Separate harnesses cover:

• non-ZST no-op cases
• ZST early return, including a nontrivially aligned ZST
• both memmove directions and the buffer-capacity boundary
• single-cycle and multiple-cycle GCD paths
• the large-element GCD dispatch
• both directions of the block-swap algorithm

The non-ZST configurations use fixed lengths and rotation amounts because a single symbolic harness covering all nested rotate paths did not complete in practice.

Notes

• Most symbolic slices are prefixes of fixed backing arrays, so their lengths are bounded rather than literally unbounded.
• Kani verifies concrete monomorphizations. The harnesses therefore use a representative type matrix rather than one non-monomorphized proof for arbitrary T.
• Const-generic APIs are checked at representative values of N.
• partition_dedup_by<()> is disabled because CBMC cannot register a zero-byte slice in the loop write set.
• swap_unchecked<()> uses a plain proof with the same documented preconditions because the contract write-set machinery has the same zero-byte-region limitation.

Verification

All added Challenge 17 harnesses pass locally with Kani.

Resolves #281

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