Add Challenge 16: Iterator

doc/src/SUMMARY.md

@@ -29,5 +29,6 @@
   - [13: Safety of `CStr`](./challenges/0013-cstr.md)
   - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)
   - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)
+  - [16: Verify the safety of Iterator functions](./challenges/0016-iter.md)
   - [17: Verify the safety of slice functions](./challenges/0017-slice.md)
   - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter-pt1.md)

doc/src/challenges/0016-iter.md

@@ -0,0 +1,74 @@
+# Challenge 16: Verify the safety of Iterator functions
+
+- **Status:** Open
+- **Tracking Issue:** [#280](https://github.com/model-checking/verify-rust-std/issues/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](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* 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](../general-rules.md)
+in addition to the ones listed above.