update SUMMARY.md, separate safe/unsafe functions

Author: thanhnguyen-aws

doc/src/SUMMARY.md

@@ -29,3 +29,4 @@
   - [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)

doc/src/challenges/0016-iter.md

@@ -17,39 +17,45 @@ Verify the safety of iter functions that are defined in (library/core/src/iter/a
 
 ### Success Criteria
 
-Write and prove the contract for the safety of the following functions:
+Write and prove the contract for the safety of the following unsafe functions:
 
 | Function | Defined in |
 |---------| ---------|
-|next_back_remainder| array_chunks.rs|
-|fold| array_chunks.rs|
 |__iterator_get_unchecked| clone.rs|
-|fold| clone.rs|
 |next_unchecked| clone.rs|
 |__iterator_get_unchecked| copied.rs|
-|spec_next_chunk| copied.rs|
 |__iterator_get_unchecked| enumerate.rs|
-|next_chunk| filter.rs|
-|next_chunk| filter_map.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 UB for following safe functions:
+
+| 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|
-|__iterator_get_unchecked | skip.rs|
 |original_step | step_by.rs|
 |spec_fold| take.rs|
 |spec_for_each| take.rs|
-|__iterator_get_unchecked | zip.rs|
-|get_unchecked| zip.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).