Add Challenge 16: Iterator

doc/src/challenges/0016-integer-arith-correctness.md

@@ -0,0 +1,55 @@
+# Challenge 16: Correctness of primitive integer types' arithmetic functions
+
+- **Status:** Open
+- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *N/A*
+
+-------------------
+
+## Goal
+
+Verify the correctness of primitive integer types' arithmetic functions in `core::num::mod.rs`.
+
+For this challenge, you can assume that all the intrinsic functions are correct.
+
+
+### Success Criteria
+
+Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types
+`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}`
+
+| Functions |
+|--------- |
+|  `checked_add`   |
+|  `saturating_add`  |
+|  `unchecked_add`   |
+|  `overflowing_add` |
+|  `wrapping_add`   |
+
+And similar versions for `sub`, `mul`, `abs`, `neg`, `pow`, `rem`, `div` (if available).
+
+| More functions |
+|--------- |
+|  `pow`   |
+|  `rem_euclid`  |
+|  `div_euclid`   |
+|  `div_ceil` |
+|  `div_floor`   |
+|  `ilog2`   |
+|  `ilog10`   |
+
+### List of UBs
+
+In addition to any properties called out as `SAFETY` comments in the source
+code,
+all proofs must automatically ensure the absence of the following [undefined behaviors](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.
+* 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/0017-integer-bit-correctness.md

@@ -0,0 +1,64 @@
+# Challenge 17: Correctness of primitive integer types' bit functions
+
+- **Status:** Open
+- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *N/A*
+
+-------------------
+
+## Goal
+
+Verify the correctness of primitive integer types' functions in `core::num::mod.rs`.
+
+For this challenge, you can assume that all the intrinsic functions are correct.
+
+### Success Criteria
+
+Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types
+`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}`
+
+| Function |
+|--------- |
+|  `checked_shl`   |
+|  `saturating_shl`  |
+|  `unchecked_shl`   |
+|  `overflowing_shl` |
+|  `wrapping_shl`   |
+|  `unbounded_shr`   |
+|  `checked_shr`   |
+|  `saturating_shr`  |
+|  `unchecked_shr`   |
+|  `overflowing_shr` |
+|  `wrapping_shr`   |
+|  `unbounded_shr`   |
+|  `swap_bytes`|
+|  `reverse_bits`|
+|  `rotate_left`|
+|  `rotate_right`|
+| `to_be` |
+| `to_le` |
+| `to_be_bytes` |
+| `to_le_bytes` |
+| `trailing_zeros` |
+| `trailing_ones` |
+| `leading_zeros` |
+| `leading_ones` |
+| `count_zeros` |
+| `count_ones` |
+
+
+### List of UBs
+
+In addition to any properties called out as `SAFETY` comments in the source
+code,
+all proofs must automatically ensure the absence of the following [undefined behaviors](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.
+* 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-nonzero-correctness.md

@@ -0,0 +1,86 @@
+# Challenge 19: Correctness of `NonZero` functions
+
+- **Status:** Open
+- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *N/A*
+
+-------------------
+
+## Goal
+
+Verify the correctness of `NonZero` functions in `core::num`.
+
+### Assumptions
+
+This challenge is the continuation of Challenge 12: Safety of `NonZero` and Challenge 14: Safety of Primitive Conversions.
+
+Now, you need to verify the "correctness" of the functions listed in Challenge 12.
+
+HOWEVER, You DON'T need to prove the "correctness" from the functions' descriptions, you JUST need to prove that those functions are consistent with those of 
+the primitive integer types (under safety preconditions of Challenge 12).
+
+For example, for the `max` function, you need to prove that 
+`∀ T in {isize, i8, i16, ... , usize, u8, ... },  ∀ x, y : NonZero<T>, x.max(y).get() == x.get().max(y.get())`
+
+Proving the correctness of the functions of primitive integer types is proposed in Challenge 16 and 17.
+
+### Success Criteria
+
+Verify that the following functions and methods (all located within `core::num::nonzero`) are consistent with those of all of the primitive integer types:
+
+| Function |
+|--------- |
+|  `max`   |
+|  `min`   |
+|  `clamp`   |
+|  `bitor`  (all 3 implementations) |
+|  `count_ones`   |
+|  `rotate_left`   |
+|  `rotate_right`   |
+|  `swap_bytes`   |
+|  `reverse_bits`   |
+|  `from_be`   |
+|  `from_le`   |
+|  `to_be`   |
+|  `to_le`   |
+|  `checked_mul`   |
+|  `saturating_mul`   |
+|  `unchecked_mul`   |
+|  `checked_pow`   |
+|  `saturating_pow`   |
+|  `neg`   |
+|  `checked_add`   |
+|  `saturating_add`   |
+|  `unchecked_add`   |
+|  `checked_next_power_of_two`   |
+|  `midpoint`   |
+|  `isqrt`   |
+|  `abs`   |
+|  `checked_abs`   |
+|  `overflowing_abs`   |
+|  `saturating_abs`   |
+|  `wrapping_abs`   |
+|  `unsigned_abs`   |
+|  `checked_neg`   |
+|  `overflowing_neg`   |
+|  `wrapping_neg` |
+|  `from_mut`   |
+|  `from_mut_unchecked` |
+
+
+### List of UBs
+
+In addition to any properties called out as `SAFETY` comments in the source
+code,
+all proofs must automatically ensure the absence of the following [undefined behaviors](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.
+* 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/0019-silce.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.
+
+It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc.
+
+### 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/0020-slice-iter.md

@@ -0,0 +1,64 @@
+# Challenge 21: Verify the memory safety and functional correctness of `slice` iter 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 functional correctness of [`std::slice` iter functions] (https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/iter/macros.rs).
+
+
+### Success Criteria
+
+The memory safety of the following public functions that iterating over the internal inductive data type must be verified:
+
+| 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.
+
+It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc.
+
+### 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.