Add Challenges 17 18 for slices

doc/src/SUMMARY.md

@@ -29,3 +29,5 @@
   - [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)
+  - [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/0017-slice.md

@@ -0,0 +1,83 @@
+# Challenge 17: Verify the safety of `slice` functions
+
+- **Status:** Open
+- **Tracking Issue:** [#281](https://github.com/model-checking/verify-rust-std/issues/281)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *10000 USD*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of `std::slice` functions in (library/core/src/slice/mod.rs).
+
+
+### Success Criteria
+
+For the following unsafe functions (in library/core/src/slice/mod.rs):
+- Write contracts specifying the safety precondition(s) that the caller must uphold, then
+- Verify that if the caller respects those preconditions, the function does not cause undefined behavior.
+
+| Function |
+|---------|
+|get_unchecked| 
+|get_unchecked_mut| 
+|swap_unchecked| 
+|as_chunks_unchecked| 
+|as_chunks_unchecked_mut| 
+|split_at_unchecked| 
+|split_at_mut_unchecked| 
+|align_to|
+|align_to_mut|
+|get_disjoint_unchecked_mut|
+
+Prove that the following safe abstractions (in library/core/src/slice/mod.rs) do not cause undefined behavior:
+
+| Function |
+|---------|
+|first_chunk| 
+|first_chunk_mut| 
+|split_first_chunk|
+|split_first_chunk_mut| 
+|split_last_chunk|
+|split_last_chunk_mut| 
+|last_chunk| 
+|last_chunk_mut| 
+|reverse| 
+|as_chunks| 
+|as_chunks_mut| 
+|as_rchunks| 
+|split_at_checked| 
+|split_at_mut_checked| 
+|binary_search_by| 
+|partition_dedup_by|
+|rotate_left|
+|rotate_right|
+|copy_from_slice|
+|copy_within|
+|swap_with_slice|
+|as_simd|
+|as_simd_mut|
+|get_disjoint_mut|
+|get_disjoint_check_valid|
+|as_flattened|
+|as_flattened_mut|
+
+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.

doc/src/challenges/0018-slice-iter.md

@@ -0,0 +1,138 @@
+# Challenge 18: Verify the safety of `slice` iter functions
+
+- **Status:** Open
+- **Tracking Issue:** [#282](https://github.com/model-checking/verify-rust-std/issues/282)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *10000 USD*
+
+-------------------
+
+
+## Goal
+**Part 1:**
+Verify the safety of Iterator functions of `std::slice` generated by `iterator!` and `forward_iterator!` macros that are defined in (library/core/src/slice/iter/macros.rs):
+to generate impl for Iter, IterMut, SplitN, SplitNMut, RSplitN, RSplitNMut  in (library/core/src/slice/iter.rs):
+
+```
+iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, as_ref, {
+    fn is_sorted_by<F>(self, mut compare: F) -> bool
+    where
+        Self: Sized,
+        F: FnMut(&Self::Item, &Self::Item) -> bool,
+    {
+        self.as_slice().is_sorted_by(|a, b| compare(&a, &b))
+    }
+}}
+
+iterator! {struct IterMut -> *mut T, &'a mut T, mut, {mut}, as_mut, {}}
+
+forward_iterator! { SplitN: T, &'a [T] }
+forward_iterator! { RSplitN: T, &'a [T] }
+forward_iterator! { SplitNMut: T, &'a mut [T] }
+forward_iterator! { RSplitNMut: T, &'a mut [T] }
+```
+
+**Part 2:**
+Verify the safety of Iterator functions of `std::slice` that are defined in (library/core/src/slice/iter.rs).
+
+### Success Criteria
+
+**Part 1:** In (library/core/src/slice/iter/macros.rs)
+
+Prove absence of undefined behaviors of following safe functions that contain unsafe code:
+
+| Function | 
+|---------|
+|make_slice| 
+|len|
+|is_empty|
+|next|
+|size_hint| 
+|count| 
+|nth| 
+|advance_by| 
+|last| 
+|fold| 
+|for_each| 
+|position| 
+|rposition| 
+|next_back| 
+|nth_back| 
+|advance_back_by| 
+
+
+**Part 2:** In (library/core/src/slice/iter.rs)
+
+Write and prove the contract for the safety of the following unsafe functions:
+
+| Function | Impl for |
+|---------| ---------|
+|__iterator_get_unchecked| Windows|
+|__iterator_get_unchecked| Chunks|
+|__iterator_get_unchecked| ChunksMut|
+|__iterator_get_unchecked| ChunksExact|
+|__iterator_get_unchecked| ChunksExact|
+|__iterator_get_unchecked| ArrayChunks|
+|__iterator_get_unchecked| ArrayChunksMut|
+|__iterator_get_unchecked| RChunks|
+|__iterator_get_unchecked| RChunksMut|
+|__iterator_get_unchecked| RChunksExact|
+|__iterator_get_unchecked| RChunksExactMut|
+
+Prove absence of undefined behaviors of following safe functions that contain unsafe code:
+
+| Function | Impl for |
+|---------| ---------|
+|new| Iter|
+|new| IterMut|
+|into_slice| IterMut|
+|as_mut_slice| IterMut|
+|next| Split|
+|next_back| Split|
+|next_back| Chunks|
+|next| ChunksMut|
+|nth| ChunksMut|
+|next_back| ChunksMut|
+|nth_back| ChunksMut|
+|new| ChunksExact|
+|new| ChunksExactMut|
+|next| ChunksExactMut|
+|nth| ChunksExactMut|
+|next_back| ChunksExactMut|
+|nth_back| ChunksExactMut|
+|next| ArrayWindows|
+|nth| ArrayWindows|
+|next_back| ArrayWindows|
+|nth_back| ArrayWindows|
+|next| RChunks|
+|next_back| RChunks|
+|next| RChunksMut|
+|nth| RChunksMut|
+|last| RChunksMut|
+|next_back| RChunksMut|
+|nth_back| RChunksMut|
+|new| RChunksExact|
+|new| RChunksExactMut|
+|next| RChunksExactMut|
+|nth| RChunksExactMut|
+|next_back| RChunksExactMut|
+|nth_back| RChunksExactMut|
+
+
+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.