0016-iter.md

Challenge 16: Verify the safety of Iterator functions

• Status: Open
• Tracking Issue: #280
• Start date: 2025-03-07
• End date: 2025-10-17
• Reward: 5000 USD

---

Goal

Verify the safety of iter functions that are defined in (library/core/src/iter/adapters):

Success Criteria

Write and prove the contract for the safety of the following unsafe functions:

Function	Defined in
__iterator_get_unchecked	clone.rs
next_unchecked	clone.rs
__iterator_get_unchecked	copied.rs
__iterator_get_unchecked	enumerate.rs
__iterator_get_unchecked	fuse.rs
__iterator_get_unchecked	map.rs
next_unchecked	map.rs
__iterator_get_unchecked	skip.rs
__iterator_get_unchecked	zip.rs
get_unchecked	zip.rs

Prove the absence of UB for following safe functions:

Function	Defined in
next_back_remainder	array_chunks.rs
fold	array_chunks.rs
spec_next_chunk	copied.rs
next_chunk_dropless	filter.rs
next_chunk	filter_map.rs
as_array_ref	map_windows.rs
as_uninit_array_mut	map_windows.rs
push	map_windows.rs
drop	map_windows.rs
original_step	step_by.rs
spec_fold	take.rs
spec_for_each	take.rs
fold	zip.rs
next	zip.rs
nth	zip.rs
next_back	zip.rs
spec_fold	zip.rs

The verification must be unbounded---it must hold for slices of arbitrary length.

The verification must hold for generic type T (no monomorphization).

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory except for padding or unions.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.