Verify safety of slice functions (Challenge 17)

[jrey8343]

Summary

Unbounded verification of 10 unsafe functions (with safety contracts) and 16+ safe functions containing unsafe code in library/core/src/slice/mod.rs, plus 128 align_to/align_to_mut harnesses across all primitive type combinations, using Kani with loop contracts (-Z loop-contracts).

Unsafe Functions with Contracts

Function	Contract (#[requires])
swap_unchecked	a < self.len() && b < self.len()
as_chunks_unchecked	N != 0 && self.len() % N == 0
as_chunks_unchecked_mut	N != 0 && self.len() % N == 0
split_at_unchecked	mid <= self.len()
split_at_mut_unchecked	mid <= self.len()
get_unchecked (usize)	idx < self.len()
get_unchecked_mut (usize)	idx < self.len()
get_unchecked (Range)	start <= end && end <= self.len()
get_unchecked_mut (Range)	start <= end && end <= self.len()
get_disjoint_unchecked_mut	indices valid and disjoint
align_to	Complex alignment + ZST contracts with #[ensures]
align_to_mut	Same as align_to

Safe Functions Verified

first_chunk, first_chunk_mut, split_first_chunk, split_first_chunk_mut, split_last_chunk, split_last_chunk_mut, last_chunk, last_chunk_mut, reverse, as_chunks, as_chunks_mut, as_rchunks, as_rchunks_mut, split_at_checked, split_at_mut_checked, binary_search_by, partition_dedup_by, rotate_left, rotate_right, copy_from_slice, copy_within, swap_with_slice, as_simd, as_simd_mut, get_disjoint_mut, get_disjoint_check_valid, as_flattened, as_flattened_mut

Coverage

~180 proof harnesses total:

• 128 align_to/align_to_mut harnesses (8×8 source/destination type pairs × 2)
• ~50 harnesses for other functions

Unbounded Verification Approach

All harnesses run without #[kani::unwind(N)]:

1. binary_search_by: The while size > 1 loop is abstracted under #[cfg(kani)] — picks a nondeterministic base in [0, len), then exercises get_unchecked(base), hint::assert_unchecked(base < len), and hint::assert_unchecked(result <= len). The unsafe ops' safety depends only on base < len, not on the search algorithm.

2. partition_dedup_by: The while next_read < len loop is abstracted under #[cfg(kani)] — executes one iteration (exercising ptr.add, &mut *ptr_read, &mut *prev_ptr_write, mem::swap) then advances to a nondeterministic valid end state.

3. reverse: Uses #[safety::loop_invariant(i <= n)] with #[kani::loop_modifies] — Kani's built-in loop contract system.

4. rotate_left/right: The internal ptr_rotate is stubbed with a no-op (#[kani::stub]) — the harnesses verify that the callers compute correct arguments.

Generic T Approach

The challenge requires verification for generic type T. Our approach:

1. Function contracts are generic: All #[requires]/#[ensures] contracts are expressed in terms of self.len(), indices, and alignment — they don't depend on T.

2. align_to/align_to_mut: Verified across 8×8 = 64 source/destination type combinations (u8, u16, u32, u64, u128, bool, char, ()) — covering all primitive alignments and sizes.

3. Other functions: Verified with u8 as a representative type. The unsafe pointer arithmetic (ptr.add, ptr::copy, get_unchecked) depends only on size_of::<T>() and align_of::<T>(), not on T's specific type. The safety invariants (index bounds, allocation validity) are identical for all T.

Key Techniques

1. #[kani::proof_for_contract] — proves contracts against implementation
2. #[kani::stub] — stubs ptr_rotate and swap_nonoverlapping to avoid CBMC intractability
3. kani::slice::any_slice_of_array — creates symbolic subslices with nondeterministic bounds
4. #[cfg(kani)] loop abstractions — eliminates loops in binary_search_by and partition_dedup_by

All harnesses pass with no --unwind and no #[kani::unwind].

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.

[jrey8343]

Note on "no monomorphization" requirement: We've asked for clarification on the tracking issue about whether Kani's representative-types approach (4 types covering all layout categories: ZST, small, validity-constrained, compound) satisfies this requirement. Kani fundamentally monomorphizes, so a VeriFast-based alternative is also being explored. See the tracking issue for details.

[jrey8343]

Update on "generic T" requirement:

While awaiting committee guidance on #281 regarding whether Kani's representative-type approach satisfies the "no monomorphization" requirement, we're also pursuing a VeriFast-based solution.

VeriFast's separation logic proofs are parametric over generic T, which would fully satisfy the requirement. However, VeriFast currently lacks &[T] support (verifast/verifast#997). We've submitted a PR to add it: verifast/verifast#1001.

Current plan:

• This PR (Kani harnesses) is valid if representative types are accepted
• If VeriFast merges &[T] support, we'll add separation logic proofs for the full generic-T coverage
• Converting to draft until the path forward is clear