Add challenge 23 24 for Vec

doc/src/SUMMARY.md

@@ -29,3 +29,5 @@
   - [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)
+  - [23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md)
+  - [24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md)

doc/src/challenges/0023-vec-pt1.md

@@ -0,0 +1,78 @@
+# Challenge 23: Verify the safety of `Vec` functions part 1
+
+- **Status:** Open
+- **Tracking Issue:** [#284](https://github.com/model-checking/verify-rust-std/issues/284)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *10000 USD*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of `std::Vec` functions (library/alloc/src/vec/mod.rs).
+
+
+### Success Criteria
+
+Verify the safety of the following public functions in (library/alloc/src/vec/mod.rs):
+
+| Function |
+|---------|
+|from_raw_parts| 
+|from_nonnull|
+|from_nonnull_in|
+|into_raw_parts_with_alloc|
+|into_boxed_slice|
+|truncate|
+|set_len|
+|swap_remove|
+|insert|
+|remove|
+|retain_mut|
+|dedup_by|
+|push|
+|push_within_capacity|
+|pop|
+|append|
+|append_elements|
+|drain|
+|clear|
+|split_off|
+|leak|
+|spare_capacity_mut|
+|split_at_spare_mut|
+|split_at_spare_mut_with_len|
+|extend_from_within|
+|into_flattened|
+|extend_with|
+|spec_extend_from_within|
+|deref|
+|deref_mut|
+|into_iter|
+|extend_desugared|
+|extend_trusted|
+|extract_if|
+|drop|
+|try_from|
+
+
+
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must 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.

doc/src/challenges/0024-vec-pt2.md

@@ -0,0 +1,67 @@
+# Challenge 24: Verify the safety of `Vec` functions part 2
+
+- **Status:** Open
+- **Tracking Issue:** [#285](https://github.com/model-checking/verify-rust-std/issues/285)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *10000 USD*
+
+-------------------
+
+
+## Goal
+
+Continue from part 1 (Challenge 23), for this challenge, you need to verify the safety of `std::Vec` iterator functions in other files in (library/alloc/src/vec/).
+
+
+### Success Criteria
+
+Verify the safety of the following functions that in implemented for `IntoIter` in (library/alloc/src/vec/into_iter.rs):
+
+| Function |
+|---------|
+|as_slice|
+|as_mut_slice|
+|forget_allocation_drop_remaining|
+|into_vecdeque|
+|next|
+|size_hint|
+|advance_by|
+|next_chunk|
+|fold|
+|try_fold|
+|__iterator_get_unchecked|
+|next_back|
+|advance_back_by|
+|drop|
+
+and the following functions from other files: 
+
+| Function | in File|
+|---------|---------|
+|next| extract_if.rs|
+|spec_extend (for IntoIter) | spec_extend.rs |
+|spec_extend (for slice::Iter) | spec_extend.rs |
+|from_elem (for i8)| spec_from_elem.rs |
+|from_elem (for u8)| spec_from_elem.rs |
+|from_elem (for ())| spec_from_elem.rs |
+|from_iter| spec_from_iter.rs|
+|from_iter (default)| spec_from_iter_nested.rs|
+
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must 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.