Challenge 25: Verify safety of VecDeque

[Samuelsills]

Summary

Verify all 43 functions listed in Challenge 25. 44 Kani proof harnesses, 0 failures.

Part A (13 unsafe functions): Safety contracts and proof_for_contract harnesses for buffer_read, buffer_write, buffer_range, push_unchecked, copy, copy_nonoverlapping, copy_slice, wrap_copy, write_iter, write_iter_wrapping, handle_capacity_increase, from_contiguous_raw_parts_in, abort_shrink.

Part B (30 safe abstractions): Proof harnesses for get, get_mut, swap, reserve, try_reserve, shrink_to, truncate, as_slices, as_mut_slices, range, range_mut, drain, pop_front, pop_back, push_front, push_back, insert, remove, split_off, append, retain_mut, grow, resize_with, make_contiguous, rotate_left, rotate_right, and others.

All harnesses exercise returned values to ensure full unsafe path coverage.

Resolves #286

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Samuelsills]

Verification Coverage Report

Unsafe Functions (13/13 — contracts written and verified)

#	Function	Verified
1	push_unchecked	✅
2	buffer_read	✅
3	buffer_write	✅
4	buffer_range	✅
5	copy	✅
6	copy_nonoverlapping	✅
7	wrap_copy	✅
8	copy_slice	✅
9	write_iter	✅
10	write_iter_wrapping	✅
11	handle_capacity_increase	✅
12	from_contiguous_raw_parts_in	✅
13	abort_shrink	✅

Safe Abstractions (30/30 — absence of UB verified)

#	Function	Verified
1-30	get, get_mut, swap, reserve_exact, reserve, try_reserve_exact, try_reserve, shrink_to, truncate, as_slices, as_mut_slices, range, range_mut, drain, pop_front, pop_back, push_front, push_back, insert, remove, split_off, append, retain_mut, grow, resize_with, make_contiguous, rotate_left, rotate_right, rotate_left_inner, rotate_right_inner	✅ All 30

UBs Checked (automatic via Kani/CBMC)

• ✅ Accessing dangling or misaligned pointers
• ✅ Reading from uninitialized memory
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• 44 proof harnesses total
• Generic type T instantiated as concrete types for tractability
• CBMC exhaustively checks all pointer operations for the listed UBs

[Copilot]

Pull request overview

This PR adds Kani-focused safety contracts (#[requires]) and proof harnesses to validate the safety of a large set of VecDeque operations, and updates the Challenge 25 documentation with a verification summary.

Changes:

• Added #[requires] contracts (and some #[kani::modifies] annotations) to several internal VecDeque unsafe fns.
• Added a substantial #[cfg(kani)] verification module with #[kani::proof] and #[kani::proof_for_contract] harnesses for VecDeque.
• Updated the Challenge 25 markdown with a “Verification Summary” and mapping of functions to harnesses/contracts.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 6 comments.

File	Description
library/alloc/src/collections/vec_deque/mod.rs	Adds safety contracts to VecDeque internals and introduces many Kani proof harnesses in mod verify.
doc/src/challenges/0025-vecdeque.md	Adds a verification summary section and tables describing covered functions/contracts/harnesses.

Comments suppressed due to low confidence (1)

library/alloc/src/collections/vec_deque/mod.rs:517

• write_iter writes to dst + i for every element yielded by iter without any bounds check, but its #[requires] only enforces dst < capacity(). The contract should capture the stated safety requirement that the iterator yields no more than capacity() - dst items (e.g., via an upper-bound from size_hint() or by requiring an ExactSizeIterator/TrustedLen), otherwise the contract is unsound and the body can write past the buffer.

    /// Writes all values from `iter` to `dst`.
    ///
    /// # Safety
    ///
    /// Assumes no wrapping around happens.
    /// Assumes capacity is sufficient: `dst + iter.len() <= capacity`.
    #[inline]
    #[requires(dst < self.capacity())]
    #[cfg_attr(kani, kani::modifies(
        core::ptr::slice_from_raw_parts_mut(self.ptr(), self.capacity()),
        written
    ))]
    unsafe fn write_iter(
        &mut self,
        dst: usize,
        iter: impl Iterator<Item = T>,
        written: &mut usize,
    ) {
        iter.enumerate().for_each(|(i, element)| unsafe {
            self.buffer_write(dst + i, element);
            *written += 1;
        });

[Copilot]

ensures is imported but never used in this module. This will trigger an unused-import warning in builds that lint warnings as errors; consider removing ensures from the import list or adding an #[allow(unused_imports)] on this use if intentional.

Suggested change

	use safety::{ensures, requires};
	use safety::requires;

[Copilot]

The safety contract for buffer_read is too weak for the operation it performs. ptr::read(self.ptr().add(off)) is UB if the slot at off is uninitialized (even if off < capacity()), so the precondition/docs should also require that off refers to an initialized element (e.g., corresponds to some logical index < self.len).

[Copilot]

write_iter_wrapping’s #[requires] is missing the key safety assumption documented in the comment: that iter yields at most len items. Without that, the calls to write_iter can still write past the end of the ring buffer. Consider expressing an iterator upper bound in the contract (or changing the function to accept an iterator with a known length).

[Copilot]

handle_capacity_increase uses old_capacity - self.head and other arithmetic assuming self.head < old_capacity (or old_capacity == 0). The current #[requires] doesn’t constrain self.head relative to old_capacity, so callers satisfying the stated preconditions can still trigger underflow and subsequent out-of-bounds copies. Consider strengthening the contract (and safety docs) to include old_capacity == 0 || self.head < old_capacity.

Suggested change

	#[inline]
	#[requires(old_capacity <= self.capacity() && self.len <= old_capacity)]
	/// Additionally, `old_capacity == 0` or `self.head < old_capacity` must hold.
	#[inline]
	#[requires(
	old_capacity <= self.capacity()
	&& self.len <= old_capacity
	&& (old_capacity == 0 || self.head < old_capacity)
	)]

[Copilot]

The verification summary claims "All 13 Part A unsafe functions" were verified, but the table lists 15 functions (it includes rotate_left_inner and rotate_right_inner). Please reconcile the counts/text so the summary matches what’s actually covered.

Suggested change

	Note: The core Part A includes 13 unsafe functions. The two internal helpers
	`rotate_left_inner` and `rotate_right_inner` are listed here and verified as
	well, but are not counted among those 13 Part A unsafe functions.

[Copilot]

The copy safety contract only constrains src/dst/len to be in-bounds, but ptr::copy(self.ptr().add(src), ...) also requires the source range to be initialized for T (reading uninitialized T is UB). If the intent is to fully formalize the unsafe preconditions, the contract/docs should also state that src..src+len refers to initialized elements in the buffer (and that the destination is valid for writes).