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.

[Copilot]

Pull request overview

Adds Kani verification for Challenge 17 slice operations.

Changes:

• Adds safety contracts to five unsafe slice methods.
• Adds concrete Kani harnesses for unsafe and safe slice APIs.
• Covers pointer operations, chunking, searching, copying, rotation, and deduplication.

Suppressed comments (2)

library/core/src/slice/mod.rs:5620

• get_unchecked_mut is also left with only assumed plain proofs rather than the required safety contract and proof_for_contract verification. Besides failing the unsafe-function criterion, the two selected index shapes do not establish the property for all supported SliceIndex implementations. Please provide the generic in-bounds contract and verify the function through it.

            #[kani::proof]

library/core/src/slice/mod.rs:5708

• This leaves get_disjoint_unchecked_mut without the contract required by Challenge 17 and proves only usize cases. Here the existing GetDisjointMutIndex::{is_in_bounds,is_overlapping} methods (or get_disjoint_check_valid) already expose the exact borrowed predicates needed for a contract, including Range and RangeInclusive; attach that precondition to the unsafe function and use proof_for_contract instead of assuming selected N/index configurations.

    #[kani::proof]

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Challenge 17 review — PR #603

Soundness (no fatal issues found)

This PR is verification-sound. I checked every item on the soundness checklist:

• cfg-swap vacuity: 0. No cfg-swapped bodies or trick attributes.
• Assume-precondition vs assume-conclusion: The kani::assume(...) calls in the plain proofs assume the documented caller preconditions (e.g. check_get_unchecked_usize_*: assume(idx < slice.len()) before get_unchecked(idx); check_get_disjoint_unchecked_mut_*: idx < len + pairwise !=). These are legitimate precondition assumptions, not assuming the conclusion. Sound.
• Trivial invariants: none; no loop_invariant(true).
• Contract liveness / faithfulness: The 5 new #[requires] are faithful to the documented safety preconditions and each is exercised by a real #[kani::proof_for_contract]:
  • slice/mod.rs:948 swap_unchecked → #[requires(a < self.len() && b < self.len())] + kani::modifies(self) (proof_for_contract, u8/u16/u64/char).
  • slice/mod.rs:1347 / :1508 as_chunks_unchecked{,_mut} → #[requires(N != 0 && self.len() % N == 0)] (proof_for_contract).
  • slice/mod.rs:2047 / :2102 split_at{,_mut}_unchecked → #[requires(mid <= self.len())] (proof_for_contract).
    None are decorative. The as_simd/as_simd_mut plain proofs correctly replay align_to's real body (no contract stubbing at the call site), so the transmute is genuinely verified.
• Over-constrained assumes: none; the assumes match the exact documented obligations.

Credit vs the rejected #567

This is substantially better than #567 and does not repeat its main failures:

• It adds 5 real, verified contracts (#567 added zero).
• It uses kani::slice::any_slice_of_array{,_mut}, i.e. a symbolic length in 0..=ARR_SIZE exercising all lengths up to the cap — not #567's single fixed len == 5.
• Safe-abstraction coverage is comprehensive: first/last/split_first/split_last chunk (+mut), as_chunks/as_chunks_mut/as_rchunks, split_at_checked/split_at_mut_checked, binary_search_by (nondet comparator, unwind(7) for len 32), partition_dedup_by, rotate_left/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. All 27 required safe fns are hit (reverse pre-exists).
• align_to/align_to_mut are already covered on main (contracts at slice/mod.rs:4070/:4168, proof_for_contract harnesses at :5426–:5504), so unlike #567 this challenge area is not left with them missing.

Blocking issues

1. Three required unsafe functions receive NO contract (hard-criterion miss).
Challenge 17 states verbatim: for each listed unsafe fn, "Write contracts specifying the safety precondition(s)... then Verify that if the caller respects those preconditions, the function does not cause UB." These three get only assume-guarded plain proofs, not contracts:

• get_unchecked (slice/mod.rs:~5592)
• get_unchecked_mut (slice/mod.rs:~5620)
• get_disjoint_unchecked_mut (slice/mod.rs:~5708)

The PR's justification (a generic SliceIndex/GetDisjointMutIndex precondition can't be written as one fn-level #[requires]) is only partly true. As Copilot notes, GetDisjointMutIndex::{is_in_bounds, is_overlapping} already expose exactly the borrowed predicates needed for a get_disjoint_unchecked_mut contract (covering Range/RangeInclusive, not just usize), and get_unchecked can carry contracts at the concrete SliceIndex impl level. So a contract is achievable and is required here. Additionally, covering only I = usize (and Range for get_unchecked) leaves the other SliceIndex impls unproven. Action: attach real safety contracts to these three and verify via proof_for_contract.

2. Bounded + monomorphized vs the verbatim mandatory criteria.
doc/src/challenges/0017-slice.md states verbatim "The verification must be unbounded---it must hold for slices of arbitrary length" and "must hold for generic type T (no monomorphization)." All harnesses use a fixed backing array (ARR_SIZE 64/100) so length is capped, and every T is a concrete monomorphization (u8/u64/char/unit/u32). The rotate_left/right harnesses are weaker still — six concrete (len, amount) configs, not even symbolic length (honestly disclosed in-comment). This is the criterion #567 was rejected on.

Fairness note for the maintainer: this bounded+concrete pattern is identical to the already-merged align_to work on main (any_slice_of_array + concrete src/dst types), so criterion #2 reflects a repo-wide tension with Kani's limits rather than a regression unique to this PR. I would not block on #2 alone. Issue #1 (missing contracts on 3 of the 10 required unsafe fns) is the concrete, actionable blocker and is why this is REQUEST_CHANGES.

Non-blocking

• No as_rchunks_mut harness, but it is not on the required list.
• swap_unchecked omits the ZST instantiation due to a documented CBMC car_set_insert limitation with modifies over zero-size regions — reasonable and disclosed; swapping ZSTs moves zero bytes.

Recommend the author add faithful contracts + proof_for_contract for get_unchecked, get_unchecked_mut, and get_disjoint_unchecked_mut, and confirm with maintainers whether the established any_slice_of_array/concrete-type encoding satisfies the unbounded+generic criteria (given it matches merged align_to), before this can be approved.