Challenge 25: Verify the safety of VecDeque (unbounded, symbolic ring layouts, contracts on all 13 unsafe fns)

[jrey8343]

Resolves #286 (Challenge 25). All changes are in library/alloc/src/collections/vec_deque/mod.rs
(plus one feature gate in library/alloc/src/lib.rs).

What is verified

• 13 unsafe functions with contracts (safety::{requires, ensures} + kani::modifies), each
  with #[kani::proof_for_contract] harnesses: push_unchecked, buffer_read, buffer_write,
  buffer_range, copy, copy_nonoverlapping, wrap_copy, copy_slice, write_iter,
  write_iter_wrapping, handle_capacity_increase, from_contiguous_raw_parts_in,
  abort_shrink; additionally rotate_left_inner / rotate_right_inner (unsafe fns on the safe
  list) carry contracts too.
• 30 safe abstractions with #[kani::proof] harnesses: 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.

How the two hard requirements are met

Unbounded. Every harness starts from any_deque(): a real allocation of symbolic capacity,
a symbolic head over every valid physical index and a symbolic len (0..=cap), with exactly
the logical range initialized. There is no kani::unwind and no length constant anywhere; the
only assumption on sizes is Layout::array::<T>(cap).is_ok() (RawVec's own precondition) and
cap * size_of::<T>() <= 2^48 (CBMC's object model under --object-bits 12, see the comment on
MAX_ALLOCATION_BYTES). Loops are discharged with loop contracts: retain_mut's two shipped
loops get attribute-only invariants, and write_iter runs its real iteration as an explicit loop
under cfg(kani) (write_iter_loop, same writes, same counting, nothing forgotten).

Wrapped states. any_deque covers both head + len <= cap and head + len > cap; every
harness reports both witnesses SATISFIED. wrap_copy has witnesses for all seven copy branches,
handle_capacity_increase for A/B/C, abort_shrink for its three outcomes, shrink_to for its
four element-moving cases, make_contiguous for all four (incl. both rotations), drain for
head/tail/interior/all.

Generic T. Harnesses are generic functions instantiated by macro: every contract harness
over u8, u64 and () (the ZST branch, capacity() == usize::MAX), the cheap ones also over
[u8; 3] (odd stride); every safe-function harness over u8 and (), the cheap ones also over
u64. As on #605 this is per-type instantiation, which Kani requires; the harness bodies
themselves are written once for arbitrary T. 125 harnesses in total.

Faithfulness notes (reviewer's list on #564/#605)

• buffer_read requires ub_checks::can_dereference(self.ptr().add(off)) (initialized slot);
  buffer_write requires can_write.
• write_iter / write_iter_wrapping bound the iterator through its upper size_hint
  (exact for the TrustedLen iterators every caller passes), and written overflow.
• handle_capacity_increase requires self.len <= old_capacity <= self.capacity() and
  self.head < old_capacity || self.head == 0.
• wrap_copy uses the documented min(|src-dst|, cap-|src-dst|) + len <= cap (which also
  implies its debug_assert!).
• abort_shrink's precondition is the state shrink_to leaves behind when the allocator unwinds.

Kani limitations worked around (all at the pinned d4df833c)

1. stub_verified on any function whose modifies names a slice ICEs (kani-compiler
   transform/contracts.rs instantiates write_any_slice with the slice type as the element
   type; Failed to stub_verified contracts with slices in kani::modifies kani#3682, fixed upstream after the pin by Fix compiler crash on slice-modifies verified stubs (#4748) kani#4749).
   kani::stub on a contracted function is blocked by #[kani::stub] on contracted functions kani#4591. Hence the
   write_iter loop lives in a contract-free cfg(kani) helper (write_iter_loop) whose
   callers are verified with a hand-written contract replacement (stub_write_iter_loop:
   asserts write_iter's precondition, havocs exactly the written slots, advances written
   and the iterator). Once the Kani pin includes auto: vim syntax highlighting improvements rust-lang/rust#4749 this can become a plain
   stub_verified(write_iter).
2. A loop contract cannot survive havocking of a loop-carried adapter holding a &mut
   (Take<ByRefSized<&mut I>> in write_iter_wrapping's wrapping branch); that is why the
   callers use the replacement above instead of running the loop.
3. Take<RepeatWith<_>> (what resize_with feeds through extend) cannot be advanced without
   a loop, so the two resize_with harnesses cover the non-wrapping append (arbitrary wrapped
   deque with capacity reserved up front, and head == 0 with growth inside resize_with); the
   wrapping write path is verified by check_write_iter_wrapping_*.
4. slice::rotate::ptr_rotate (reached from make_contiguous) is a safe callee abstracted by a
   precondition-checking stub; make_contiguous performs no value-dependent step after it.
5. CBMC 6.8 aborts on a loop_modifies target that is a zero-sized closure
   (CBMC aborts with l2_rename_rvalues case struct' not handled` when a zero-sized closure is a loop_modifies target kani#4786); the retain_mut loop contract therefore does not list the
   predicate (harness predicates are stateless).

Finding: from_contiguous_raw_parts_in is reachable with head == capacity (unsound)

Writing the contract for from_contiguous_raw_parts_in showed that vec::IntoIter::into_vecdeque
passes initialized == capacity..capacity for an exhausted iterator whose Vec had
capacity == len, producing a deque with head == capacity, outside the field comment's
head < capacity. pop_front reads slot head unwrapped, so after one push_back this reads
one past the end of the buffer (segfault demonstrated by @maxdexh). Reported as
rust-lang#162452, labelled I-unsound and claimed for a fix. The contract here requires
initialized.start < capacity || initialized.start == 0 and ensures the structural invariant,
which is exactly the precondition into_vecdeque violates; the fix upstream will make that
caller satisfy it.

Local results

125 harnesses with the pinned Kani, all passing, every kani::cover witness satisfied. Heaviest:
insert (u8) ~3-6 min, wrap_copy (u8/u64) ~2-3 min, rotate_*_inner (u8) ~2 min; total ≈ 45
CPU-minutes. -Z uninit-checks could not be used as additional evidence: at the pinned Kani it
rejects alloc (function-pointer operands, kani#3300).

🤖 Generated with Claude Code

https://claude.ai/code/session_011hQMihqVQLDerCELXExGHg