Add Kani harnesses for Challenge 18: slice iter functions

[MavenRain]

Solution to Challenge 18: verify the safety of slice iter functions.

Part 1

• All 16 functions from the iterator! macro are proved for IterMut (make_slice, len, is_empty, next, size_hint, count, nth, advance_by, last, fold, for_each, position, rposition, next_back, nth_back, advance_back_by). Iter coverage already exists on main and stays green.
• next and size_hint are proved for SplitN, SplitNMut, RSplitN, and RSplitNMut through the forward_iterator! path.

Part 2

• The current snapshot of slice/iter.rs contains 9 __iterator_get_unchecked impls: Windows, Chunks, ChunksMut, ChunksExact, ChunksExactMut, RChunks, RChunksMut, RChunksExact, RChunksExactMut. ArrayChunks and ArrayChunksMut no longer exist in this file.
• Each of the 9 gets a safety contract (#[requires]/#[ensures]) on a private contracted inherent method. The __iterator_get_unchecked trait method delegates to it. Each contract is proved with #[kani::proof_for_contract]. This pattern sidesteps the known interaction between proof_for_contract and generic trait methods.
• All safe functions with unsafe bodies from the second table have harnesses: the constructors (Iter::new, IterMut::new, ChunksExact::new, ChunksExactMut::new, RChunksExact::new, RChunksExactMut::new), IterMut::{into_slice, as_mut_slice}, the Split family, ArrayWindows, and the chunk-family next/nth/last/next_back/nth_back methods.

Approach and disclosures

• Generic code is instantiated over representative types: () (ZST), u8, char (validity invariant), and (char, u8) (padding). Kani cannot emit one proof for all T; this per-type spread is the same pattern the merged solutions for challenges 16 and 17 use.
• Element values are symbolic in every harness. Backing lengths are symbolic up to isize::MAX for () and u32::MAX for u8; char and (char, u8) use smaller symbolic bounds to keep solver time practical.
• Looping harnesses (fold, for_each, position, rposition, last, and the split families) use #[kani::unwind] bounds. Kani verifies the unwinding assertion, so a bound that is too small fails loudly.
• Verified locally at the pinned Kani commit d4df833c (toolchain nightly-2025-11-25): 385 of 385 harnesses successful, 0 failures.
• AI assistance (Claude) was used to write the harnesses. All proofs were checked locally with the pinned Kani version.

Resolves #282

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

[feliperodri]

Thanks @MavenRain. Reviewed against Challenge 18 with our vacuity tooling. Between the two open Challenge 18 solutions we're prioritizing this one — completeness is strong (Part 1 16/16 for IterMut, Part 2-A 9/9 applicable contracts genuinely proved via inherent-twin + #[kani::proof_for_contract] — which fixes the pre-existing T7 gap where base had orphan #[requires] — and Part 2-B broadly covered) and soundness is clean (no cfg(kani) body swaps, substantive is_safe() invariant, no loop_invariant(true), only benign kani::assume(ptr.is_aligned()) in a dangling branch).

Requesting changes for two reasons:

1. Fails unbounded + generic-T. Every harness is monomorphized over (), u8, char, (char,u8); the chunk-family contracts and next/nth harnesses cap at MAX_LEN=50; looping/Split harnesses at MAX_LEN=4 + unwind(5–6). Only Windows get_unchecked, ArrayWindows and IterMut O(1) methods on ()/u8 are unbounded. The challenge mandates arbitrary length and generic T throughout.
2. Runtime-logic edit to reconcile. The new inherent iterator_get_unchecked methods (and the RChunks/RChunksMut checked_sub(...).unwrap_or(0) rewrite) live in the shipping std source, not cfg(kani)-gated. Behavior-preserving, but per CLAUDE.md this repo mustn't change std runtime logic. Please either cfg(kani)-gate the refactor or land the extraction upstream first, then verify here.

Nice work on the inherent-twin trick to genuinely prove the trait-impl #[requires]. Blocker is the standing unbounded+generic-T gate (same acceptance question as Ch16/17).

[MavenRain]

Thanks for the review. I have prepared a local fix for the runtime-logic concern: all nine original trait implementations are restored, and the inherent contract wrappers are cfg(kani)-gated. Each wrapper calls the original trait method directly. This also restores the original RChunks/RChunksMut arithmetic. Source-identity and pinned rustfmt checks pass; the changed contract call path still needs proof verification before I claim a new passing result.

The arbitrary-length and generic-T requirement remains open. The existing bounded, concrete-type harnesses do not satisfy it. Pinned Kani rejects generic proof harnesses, so I investigated the approved VeriFast route using small standalone examples.

VeriFast 26.01 verifies a scalar baseline, but even this safe generic slice function fails with unsupported slice-reference ownership:

pub fn slice_len<T>(values: &[T]) -> usize
//@ req true;
//@ ens result == ptr_len(values);
//@ on_unwind_ens false;
{
    values.len()
}

The same restriction remains in the current VeriFast translator. A separate probe also found no specification for usize::unchecked_sub, used by the chunk iterators.

Is there an approved proof route or existing generic slice-ownership development you recommend for Challenge 18, or does satisfying this gate first require work on the verifier itself? I have not assumed an exception to the stated criteria.

[feliperodri]

@btj any advice about the VeriFast route here?