Challenge 16: Verify safety of iterator adapter functions with Kani

[v3risec]

Summary

This PR adds Kani-based verification for Challenge 16, covering the iterator safety targets in library/core/src/iter/adapters.

The change introduces:

• safety preconditions for all 10 unsafe functions listed by the challenge
• proof harnesses for all 10 unsafe functions and all 17 safe abstractions
• symbolic iterator lengths and indices for the random-access adapter proofs
• loop contracts for iterator loops in array_chunks.rs, skip.rs, take.rs, and zip.rs
• representative type instantiations covering signed and unsigned integers, bool, zero-sized types, and arrays

All verification-only modules and annotations are gated by cfg(kani). Normal non-Kani builds retain their existing runtime behavior.

Challenge Coverage

Requirement	Coverage	Notes
Unsafe functions	10 / 10	Safety contracts and dedicated proof harnesses
Safe functions	17 / 17	Every function listed by Challenge 16 has direct harness coverage

Unsafe functions

The following unsafe functions receive safety contracts and proof coverage:

• Cloned::__iterator_get_unchecked
• Cloned::next_unchecked
• Copied::__iterator_get_unchecked
• Enumerate::__iterator_get_unchecked
• Fuse::__iterator_get_unchecked
• Map::__iterator_get_unchecked
• Map::next_unchecked
• Skip::__iterator_get_unchecked
• Zip::__iterator_get_unchecked
• ZipImpl::get_unchecked

The challenge refers to clone.rs; the corresponding file in the current source tree is cloned.rs.

Because Kani's contract harness machinery cannot resolve several specialized trait-method paths, the proofs call those implementations through explicit trait paths and establish their preconditions with kani::assume.

Safe functions

Proof harnesses cover all safe abstractions listed by the challenge:

• ArrayChunks::next_back_remainder
• ArrayChunks::fold
• Copied::spec_next_chunk
• Filter::next_chunk_dropless
• FilterMap::next_chunk
• Buffer::as_array_ref
• Buffer::as_uninit_array_mut
• Buffer::push
• Buffer::drop
• StepBy::original_step
• Take::spec_fold
• Take::spec_for_each
• Zip::fold
• Zip::next
• Zip::nth
• Zip::next_back
• Zip::spec_fold

Verification Approach

The proofs use a combination of:

1. Symbolic iterator states
   Random-access adapter proofs use symbolic lengths, indices, pending skip counts, zip offsets, and payload values. Lazy ranges and mapped ranges allow many of these proofs to avoid imposing a harness-level length bound.

2. Safety contracts
   The unsafe functions require the requested element to be within the trusted lower bound or remaining iterator size. The Fuse contract additionally requires the inner iterator to remain present.

3. Loop contracts
   Loop invariants preserve the index and iterator-size relationships needed by unchecked accesses in ArrayChunks, Skip, Take, and Zip.

4. Specialization-aware harnesses
   The harnesses construct iterators implementing the required TrustedRandomAccess, TrustedRandomAccessNoCoerce, or TrustedLen bounds and call the specialized implementation directly where necessary.

5. Representative concrete types
   The proofs instantiate the adapters with signed and unsigned integer widths, bool, (), and [u8; 4]. MapWindows additionally exercises multiple window sizes.

Kani checks the resulting programs for invalid pointer accesses, uninitialized reads, mutation through invalid references, invalid values, arithmetic failures, and assertion violations.

Notes

• Generic type requirement: Kani verifies concrete monomorphized programs. This branch therefore uses representative concrete types rather than providing a single non-monomorphized proof for arbitrary T.

• Const-generic coverage: Chunk and window operations are exercised with representative values of N, rather than universally quantifying over every nonzero const-generic value.

• Zip::spec_fold: Under cfg(kani), the original TrustedLen loop is represented by a sound loop abstraction that nondeterministically selects an arbitrary valid iteration. Because the selected index is unconstrained within the entire range, the proof covers every possible iteration rather than only a fixed prefix. The TrustedLen invariant guarantees that both iterators contain an element at that position, so verifying the corresponding unwrap_unchecked calls establishes their safety for all loop iterations without explicitly unwinding the full loop.

Verification

All added Challenge 21 harnesses pass locally with Kani.

Resolves #280

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