add slice challenges

model-checking · Mar 6, 2025 · 72baf24 · 72baf24
1 parent b764eeb
commit 72baf24
Show file tree

Hide file tree

Showing 3 changed files with 247 additions and 0 deletions.
diff --git a/doc/src/challenges/0017-slice.md b/doc/src/challenges/0017-slice.md
@@ -0,0 +1,79 @@
+# Challenge 17: Verify the safety of `slice` functions
+
+- **Status:** Open
+- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *?*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of [`std::slice`] functions in (library/core/src/slice/mod.rs).
+
+
+### Success Criteria
+
+The memory safety of the following public functions that iterating over the internal inductive data type must be verified:
+
+| 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| 
+|get_unchecked| 
+|get_unchecked_mut| 
+|as_ptr_range| 
+|as_mut_ptr_range| 
+|as_array| 
+|as_mut_array| 
+|swap| 
+|swap_unchecked| 
+|reverse| 
+|as_chunks_unchecked| 
+|as_chunks| 
+|as_rchunks| 
+|as_chunks_unchecked_mut| 
+|split_at_unchecked| 
+|split_at_mut_unchecked| 
+|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|
+|align_to|
+|align_to_mut|
+|as_simd|
+|as_simd_mut|
+|get_many_unchecked_mut|
+|get_many_mut|
+|as_flattened|
+|as_flattened_mut|
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must be 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.
diff --git a/doc/src/challenges/0018-slice-iter-pt1.md b/doc/src/challenges/0018-slice-iter-pt1.md
@@ -0,0 +1,83 @@
+# Challenge 18: Verify the safety of `slice` iter functions - part 1
+
+- **Status:** Open
+- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *?*
+
+-------------------
+
+
+## Goal
+
+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] }
+```
+
+### Success Criteria
+
+Write and prove the contract for the safety of the following functions:
+
+| Function | 
+|---------|
+|next_back_unchecked| 
+|make_slice| 
+|pre_dec_end|
+|post_inc_start| 
+|len|
+|is_empty|
+|next|
+|size_hint| 
+|count| 
+|nth| 
+|advance_by| 
+|last| 
+|fold| 
+|for_each| 
+|all| 
+|any| 
+|find| 
+|find_map| 
+|position| 
+|rposition| 
+|next_back| 
+|nth_back| 
+|advance_back_by| 
+|next_unchecked| 
+
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must be 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.
diff --git a/doc/src/challenges/0019-slice-iter-pt2.md b/doc/src/challenges/0019-slice-iter-pt2.md
@@ -0,0 +1,85 @@
+# Challenge 19: Verify the safety of `slice` iter functions - part 2
+
+- **Status:** Open
+- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *?*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of Iterator functions of [`std::slice`] that are defined in (library/core/src/slice/iter.rs):
+
+
+
+### Success Criteria
+
+Write and prove the contract for the safety of the following functions:
+
+| Function | Impl for |
+|---------| ---------|
+|new| Iter|
+|new| IterMut|
+|into_slice| IterMut|
+|as_mut_slice| IterMut|
+|next| Split|
+|next_back| Split|
+|__iterator_get_unchecked| Windows|
+|__iterator_get_unchecked| Chunks|
+|next_back| Chunks|
+|next| ChunksMut|
+|nth| ChunksMut|
+|__iterator_get_unchecked| ChunksMut|
+|next_back| ChunksMut|
+|nth_back| ChunksMut|
+|new| ChunksExact|
+|__iterator_get_unchecked| ChunksExact|
+|new| ChunksExactMut|
+|next| ChunksExactMut|
+|nth| ChunksExactMut|
+|__iterator_get_unchecked| ChunksExact|
+|next_back| ChunksExactMut|
+|nth_back| ChunksExactMut|
+|next| ArrayWindows|
+|nth| ArrayWindows|
+|next_back| ArrayWindows|
+|nth_back| ArrayWindows|
+|__iterator_get_unchecked| ArrayChunks|
+|__iterator_get_unchecked| ArrayChunksMut|
+|next| RChunks|
+|__iterator_get_unchecked| RChunks|
+|next_back| RChunks|
+|next| RChunksMut|
+|nth| RChunksMut|
+|last| RChunksMut|
+|__iterator_get_unchecked| RChunksMut|
+|next_back| RChunksMut|
+|nth_back| RChunksMut|
+|new| RChunksExact|
+|__iterator_get_unchecked| RChunksExact|
+|new| RChunksExactMut|
+|next| RChunksExactMut|
+|nth| RChunksExactMut|
+|__iterator_get_unchecked| RChunksExactMut|
+|next_back| RChunksExactMut|
+|nth_back| RChunksExactMut|
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must be 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.