Verify safety of iterator adapter functions (Challenge 16)

[kasimte]

Summary

Resolves #280 (Challenge 16: Verify the safety of Iterator functions)

Adds 72 Kani verification harnesses proving the safety of all 10 unsafe functions and all 17 safe abstractions listed in Challenge 16, across 13 iterator adapter files in library/core/src/iter/adapters/.

Approach

• No monomorphization: 4 representative types per function — u8 (non-ZST), () (ZST), char (4-byte with validity constraints), (char, u8) (compound with padding) — to address the generic type T requirement
• Symbolic inputs via kani::slice::any_slice_of_array with MAX_LEN=8 for arbitrary-length verification
• Safety contracts (#[requires]) added where the proc macro supports it (inherent impl methods). For trait impl methods, kani::assume() preconditions are used in harnesses due to a known limitation where the safety proc macro cannot parse ImplItemFn
• next_back_remainder uses Range<u8> as inner iterator instead of slice::Iter because CBMC exhausts resources on the pointer-heavy .rev().take(rem).next_chunk() adapter chain. Range<u8> still exercises the same unwrap_err_unchecked code path

Safety contracts added

Function	File	Contract
next_unchecked	cloned.rs	#[requires(self.it.size_hint().0 > 0)]
get_unchecked	zip.rs	#[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]

Unsafe functions verified (10/10)

Function	File	Harnesses
__iterator_get_unchecked	cloned.rs	4 (u8, unit, char, tup)
next_unchecked	cloned.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	copied.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	enumerate.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	fuse.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	map.rs	4 (u8, unit, char, tup)
next_unchecked	map.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	skip.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	zip.rs	4 (u8, unit, char, tup)
get_unchecked	zip.rs	4 (shared — called transitively by __iterator_get_unchecked above)

Safe abstractions verified (17/17)

Function	File	Harnesses
next_back_remainder	array_chunks.rs	2 (N=2, N=3 via Range<u8>)
fold	array_chunks.rs	4 (N=2 u8/unit/char, N=3 u8)
spec_next_chunk	copied.rs	4 (N=2/3 u8, N=2 unit/char)
next_chunk_dropless	filter.rs	3 (N=2/3 u8, N=2 char)
next_chunk	filter_map.rs	3 (N=2/3 u8, N=2 char)
as_array_ref	map_windows.rs	4 shared (N=2/3 u8, N=2 char iteration)
as_uninit_array_mut	map_windows.rs	same 4 harnesses (exercised via Buffer::clone)
push	map_windows.rs	same 4 harnesses (exercised via iteration)
drop	map_windows.rs	same 4 harnesses (exercised via iteration)
original_step	step_by.rs	3 (size_hint u8/char, iterate u8)
spec_fold	take.rs	4 (u8, unit, char, tup)
spec_for_each	take.rs	2 (u8, char)
fold	zip.rs	2 (u8, char)
next	zip.rs	2 (u8, char)
nth	zip.rs	1 (u8)
next_back	zip.rs	1 (u8)
spec_fold	zip.rs	1 (u8 via RepeatN)

Verification

All 72 harnesses pass:

VERIFICATION: SUCCESSFUL
Manual Harness Summary:
Complete - 72 successfully verified harnesses, 0 failures, 72 total.

Run with:

./scripts/run-kani.sh --kani-args \
  --harness iter::adapters::copied::verify \
  --harness iter::adapters::cloned::verify \
  --harness iter::adapters::map::verify \
  --harness iter::adapters::enumerate::verify \
  --harness iter::adapters::fuse::verify \
  --harness iter::adapters::skip::verify \
  --harness iter::adapters::zip::verify \
  --harness iter::adapters::array_chunks::verify \
  --harness iter::adapters::filter::verify \
  --harness iter::adapters::filter_map::verify \
  --harness iter::adapters::map_windows::verify \
  --harness iter::adapters::step_by::verify \
  --harness iter::adapters::take::verify \
  --output-format terse

Test plan

• All 72 harnesses pass locally
• CI passes

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.