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:
| 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 undefined behavior for following safe abstractions:
| 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.