Challenge 16: Verify the safety of Iterator functions

  • Status: Open
  • Tracking Issue: #280
  • Start date: 2025-03-07
  • End date: 2025-10-17
  • Reward: 10,000 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:

FunctionDefined in
__iterator_get_uncheckedclone.rs
next_uncheckedclone.rs
__iterator_get_uncheckedcopied.rs
__iterator_get_uncheckedenumerate.rs
__iterator_get_uncheckedfuse.rs
__iterator_get_uncheckedmap.rs
next_uncheckedmap.rs
__iterator_get_uncheckedskip.rs
__iterator_get_uncheckedzip.rs
get_uncheckedzip.rs

Prove the absence of undefined behavior for following safe abstractions:

FunctionDefined in
next_back_remainderarray_chunks.rs
foldarray_chunks.rs
spec_next_chunkcopied.rs
next_chunk_droplessfilter.rs
next_chunkfilter_map.rs
as_array_refmap_windows.rs
as_uninit_array_mutmap_windows.rs
pushmap_windows.rs
dropmap_windows.rs
original_stepstep_by.rs
spec_foldtake.rs
spec_for_eachtake.rs
foldzip.rs
nextzip.rs
nthzip.rs
next_backzip.rs
spec_foldzip.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.