Add Challenge 25: VecDeque

doc/src/challenges/0025-vecdeque.md

@@ -0,0 +1,77 @@
+# Challenge 17: Verify the safety of `VecDeque` 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 safety of [`VecDeque`] functions in (library/alloc/src/collections/vec_deque/mod.rs).
+
+
+### Success Criteria
+
+Verify the safety of the following functions in (library/alloc/src/collections/vec_deque/mod.rs).
+
+| Function |
+|---------|
+|push_unchecked|
+|buffer_read|
+|buffer_write|
+|buffer_range|
+|copy|
+|copy_nonoverlapping|
+|wrap_copy|
+|copy_slice|
+|handle_capacity_increase|
+|from_contiguous_raw_parts_in|
+|get|
+|get_mut|
+|swap|
+|capacity|
+|reserve_exact|
+|reserve|
+|try_reserve_exact|
+|try_reserve|
+|shrink_to|
+|abort_shrink|
+|as_slices|
+|as_mut_slices|
+|range|
+|range_mut|
+|pop_front|
+|pop_back|
+|push_front|
+|push_back|
+|insert|
+|remove|
+|split_off|
+|append|
+|grow|
+|make_contiguous|
+|rotate_left|
+|rotate_right|
+|rotate_left_inner|
+|rotate_right_inner|
+
+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.