combine 2 challenges

Author: thanhnguyen-aws

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

@@ -1,4 +1,4 @@
-# Challenge 18: Verify the safety of `slice` iter functions - part 1
+# Challenge 18: Verify the safety of `slice` iter functions
 
 - **Status:** Open
 - **Tracking Issue:** [#282](https://github.com/model-checking/verify-rust-std/issues/282)
@@ -10,7 +10,7 @@
 
 
 ## 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):
 
@@ -33,16 +33,18 @@ 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
 
-Write and prove the contract for the safety of the following functions:
+**Part 1:** In (library/core/src/slice/iter/macros.rs)
+
+Prove absence of undefined behaviors of following safe functions that contain unsafe code:
 
 | Function | 
 |---------|
-|next_back_unchecked| 
 |make_slice| 
-|pre_dec_end|
-|post_inc_start| 
 |len|
 |is_empty|
 |next|
@@ -62,7 +64,64 @@ Write and prove the contract for the safety of the following functions:
 |next_back| 
 |nth_back| 
 |advance_back_by| 
-|next_unchecked| 
+
+
+**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.