fixed challenge 16

doc/src/challenges/0016-slice.md

@@ -0,0 +1,79 @@
+# Challenge 20: Verify the memory 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 memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/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.