From d41e3fa72e8ce35d0f92bed3fa4f5c280f18d7dd Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Tue, 8 Sep 2026 12:18:19 +1000 Subject: [PATCH 1/3] Verify VecDeque (Challenge 25): contracts on the 13 unsafe fns and unbounded proofs for the 30 safe fns Adds `safety::{requires, ensures}` contracts (with `kani::modifies`) to `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` (plus `rotate_left_inner` / `rotate_right_inner`), each verified by `proof_for_contract` harnesses, and `kani::proof` harnesses for the 30 safe abstractions listed in the challenge. All harnesses start from a deque with symbolic capacity, symbolic `head` and symbolic `len` (`any_deque`), so both contiguous and wrapped ring layouts are explored; no harness bounds the length or capacity, and no harness uses `kani::unwind`. Loops are handled with loop contracts: the shipped `retain_mut` loops get attribute-only invariants, and `write_iter`'s `for_each` is spelled as an equivalent explicit loop under `cfg(kani)` (`write_iter_loop`) so that a loop contract can be attached. The `slice::rotate` call in `make_contiguous` is abstracted by a precondition-checking stub. Only shipped-code changes: the `cfg(kani)` loop form of `write_iter`, the loop-contract attributes on `retain_mut`, and `#![feature(proc_macro_hygiene)]` in alloc's lib.rs (needed for statement attributes, as in core). Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_011hQMihqVQLDerCELXExGHg --- .../alloc/src/collections/vec_deque/mod.rs | 1327 ++++++++++++++++- library/alloc/src/lib.rs | 1 + 2 files changed, 1327 insertions(+), 1 deletion(-) diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index 436a05f12b909..f55e9549df798 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -21,6 +21,10 @@ use core::mem::{ManuallyDrop, SizedTypeProperties}; use core::ops::{Index, IndexMut, Range, RangeBounds}; use core::{fmt, ptr, slice}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::alloc::Layout; use crate::alloc::{Allocator, Global}; use crate::collections::{TryReserveError, TryReserveErrorKind}; use crate::raw_vec::RawVec; @@ -170,12 +174,42 @@ impl VecDeque { self.buf.ptr() } + /// Structural invariant of a `VecDeque` (see the field comments on the struct): + /// `len <= capacity()` and `head < capacity()` unless the capacity is zero, in which + /// case `head == 0`. Only used by the verification contracts below and by `mod verify`. + #[cfg(kani)] + fn invariant_holds(&self) -> bool { + self.len <= self.capacity() + && (self.head < self.capacity() || (self.capacity() == 0 && self.head == 0)) + } + + /// The physical slots `off..off + n` as a slice pointer, for `modifies` clauses. An empty + /// range is represented by a null slice so that a dangling or one-past-the-end base pointer + /// never has to be checked for writability. Only used by the verification contracts. + #[cfg(kani)] + fn slots(&self, off: usize, n: usize) -> *mut [T] { + if n == 0 || T::IS_ZST { + ptr::slice_from_raw_parts_mut(ptr::null_mut(), 0) + } else { + ptr::slice_from_raw_parts_mut(unsafe { self.ptr().add(off) }, n) + } + } + + /// The whole physical buffer as a slice pointer, for `modifies` clauses. + #[cfg(kani)] + fn all_slots(&self) -> *mut [T] { + self.slots(0, self.capacity()) + } + /// Appends an element to the buffer. /// /// # Safety /// /// May only be called if `deque.len() < deque.capacity()` #[inline] + #[requires(self.invariant_holds() && self.len < self.capacity())] + #[ensures(|_| self.len == old(self.len) + 1 && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies(&self.len, self.slots(self.to_physical_idx(self.len), 1)))] unsafe fn push_unchecked(&mut self, element: T) { // SAFETY: Because of the precondition, it's guaranteed that there is space // in the logical array after the last element. @@ -200,7 +234,13 @@ impl VecDeque { } /// Moves an element out of the buffer + /// + /// # Safety + /// + /// `off < self.capacity()` and slot `off` must hold an initialized `T`. The value is moved + /// out: the caller must ensure the slot is no longer considered initialized afterwards. #[inline] + #[requires(off < self.capacity() && core::ub_checks::can_dereference(unsafe { self.ptr().add(off) }))] unsafe fn buffer_read(&mut self, off: usize) -> T { unsafe { ptr::read(self.ptr().add(off)) } } @@ -210,6 +250,9 @@ impl VecDeque { /// /// May only be called if `off < self.capacity()`. #[inline] + #[requires(off < self.capacity() && core::ub_checks::can_write(unsafe { self.ptr().add(off) }))] + #[ensures(|result| core::ptr::eq(*result, old(unsafe { self.ptr().add(off) })))] + #[cfg_attr(kani, kani::modifies(self.slots(off, 1)))] unsafe fn buffer_write(&mut self, off: usize, value: T) -> &mut T { unsafe { let ptr = self.ptr().add(off); @@ -221,6 +264,9 @@ impl VecDeque { /// Returns a slice pointer into the buffer. /// `range` must lie inside `0..self.capacity()`. #[inline] + #[requires(range.start <= range.end && range.end <= self.capacity())] + #[ensures(|result| result.len() == old(range.end) - old(range.start) + && core::ptr::eq(*result as *const T, unsafe { self.ptr().add(old(range.start)) }))] unsafe fn buffer_range(&self, range: Range) -> *mut [T] { unsafe { ptr::slice_from_raw_parts_mut(self.ptr().add(range.start), range.end - range.start) @@ -325,7 +371,14 @@ impl VecDeque { } /// Copies a contiguous block of memory len long from src to dst + /// + /// # Safety + /// + /// `src + len <= self.capacity()` and `dst + len <= self.capacity()`. #[inline] + #[requires(len <= self.capacity() && src <= self.capacity() - len && dst <= self.capacity() - len)] + #[ensures(|_| self.head == old(self.head) && self.len == old(self.len))] + #[cfg_attr(kani, kani::modifies(self.slots(dst, len)))] unsafe fn copy(&mut self, src: usize, dst: usize, len: usize) { debug_assert!( dst + len <= self.capacity(), @@ -349,7 +402,16 @@ impl VecDeque { } /// Copies a contiguous block of memory len long from src to dst + /// + /// # Safety + /// + /// `src + len <= self.capacity()`, `dst + len <= self.capacity()` and the two ranges + /// must not overlap: `src.abs_diff(dst) >= len`. #[inline] + #[requires(len <= self.capacity() && src <= self.capacity() - len && dst <= self.capacity() - len)] + #[requires(src.abs_diff(dst) >= len)] + #[ensures(|_| self.head == old(self.head) && self.len == old(self.len))] + #[cfg_attr(kani, kani::modifies(self.slots(dst, len)))] unsafe fn copy_nonoverlapping(&mut self, src: usize, dst: usize, len: usize) { debug_assert!( dst + len <= self.capacity(), @@ -375,6 +437,19 @@ impl VecDeque { /// Copies a potentially wrapping block of memory len long from src to dest. /// (abs(dst - src) + len) must be no larger than capacity() (There must be at /// most one continuous overlapping region between src and dest). + /// + /// # Safety + /// + /// `src` and `dst` must be physical indices (`< self.capacity()`, or both `0` when the + /// capacity is `0`) and `min(src.abs_diff(dst), self.capacity() - src.abs_diff(dst)) + len` + /// must not exceed `self.capacity()`. + #[requires(self.invariant_holds() + && ((src < self.capacity() && dst < self.capacity()) || (src == 0 && dst == 0)) + && cmp::min(src.abs_diff(dst), self.capacity() - src.abs_diff(dst)) + .checked_add(len) + .is_some_and(|end| end <= self.capacity()))] + #[ensures(|_| self.head == old(self.head) && self.len == old(self.len))] + #[cfg_attr(kani, kani::modifies(self.all_slots()))] unsafe fn wrap_copy(&mut self, src: usize, dst: usize, len: usize) { debug_assert!( cmp::min(src.abs_diff(dst), self.capacity() - src.abs_diff(dst)) + len @@ -508,7 +583,14 @@ impl VecDeque { /// Copies all values from `src` to `dst`, wrapping around if needed. /// Assumes capacity is sufficient. + /// + /// # Safety + /// + /// `dst <= self.capacity()` and `src.len() <= self.capacity()`. #[inline] + #[requires(dst <= self.capacity() && src.len() <= self.capacity())] + #[ensures(|_| self.head == old(self.head) && self.len == old(self.len))] + #[cfg_attr(kani, kani::modifies(self.all_slots()))] unsafe fn copy_slice(&mut self, dst: usize, src: &[T]) { debug_assert!(src.len() <= self.capacity()); let head_room = self.capacity() - dst; @@ -560,17 +642,71 @@ impl VecDeque { /// /// Assumes no wrapping around happens. /// Assumes capacity is sufficient. + /// + /// # Safety + /// + /// `iter` must yield at most `self.capacity() - dst` items. The contract below expresses + /// this through the iterator's upper `size_hint`, which is exact for the `TrustedLen` + /// iterators every caller passes. #[inline] + #[requires(iter.size_hint().1.is_some_and(|hi| { + dst.checked_add(hi).is_some_and(|end| end <= self.capacity()) + && written.checked_add(hi).is_some() + }))] + #[ensures(|_| old(*written) <= *written + && *written - old(*written) <= old(iter.size_hint().1.unwrap_or(0)))] + #[cfg_attr(kani, kani::modifies(written, self.slots(dst, iter.size_hint().1.unwrap_or(0))))] unsafe fn write_iter( &mut self, dst: usize, iter: impl Iterator, written: &mut usize, ) { + #[cfg(not(kani))] iter.enumerate().for_each(|(i, element)| unsafe { self.buffer_write(dst + i, element); *written += 1; }); + // Under Kani the very same iteration is spelled as an explicit loop (see + // `write_iter_loop`) so that a loop contract can be attached; loop contracts cannot be + // attached to the closure-driven `for_each`. + #[cfg(kani)] + unsafe { + self.write_iter_loop(dst, iter, written) + } + } + + /// The loop of [`Self::write_iter`] in the form Kani's loop contracts accept: every element + /// yielded by `iter` is written to `dst + i` and counted, exactly as `for_each` does above; + /// nothing is skipped, synthesized or forgotten. It is verified as part of `write_iter`'s + /// contract proof (`check_write_iter_*` in `mod verify`). Callers of `write_iter` are + /// verified with this helper replaced by its contract (`stub_write_iter_loop`), because a + /// loop contract cannot survive the havocking of the reference-carrying + /// `Take>` adapter that `write_iter_wrapping` passes. + #[cfg(kani)] + #[inline] + unsafe fn write_iter_loop( + &mut self, + dst: usize, + iter: impl Iterator, + written: &mut usize, + ) { + let bound = iter.size_hint().1.unwrap_or(0); + let written_on_entry = *written; + let mut iter = iter; + let mut i = 0; + #[safety::loop_invariant(i <= bound + && *written == written_on_entry + i + && iter.size_hint().1 == Some(bound - i))] + #[kani::loop_modifies(&raw mut *written, &i, &iter, self.slots(dst, bound))] + loop { + let Some(element) = iter.next() else { break }; + unsafe { + self.buffer_write(dst + i, element); + } + *written += 1; + i += 1; + } } /// Writes all values from `iter` to `dst`, wrapping @@ -581,6 +717,19 @@ impl VecDeque { /// /// Assumes that `iter` yields at most `len` items. /// Assumes capacity is sufficient. + /// + /// # Safety + /// + /// `dst <= self.capacity()`, `self.len + len <= self.capacity()` and `iter` yields at most + /// `len` items (expressed through its upper `size_hint`, exact for `TrustedLen` callers). + #[requires(self.invariant_holds() && dst <= self.capacity() && len <= self.capacity() - self.len)] + #[requires(iter.size_hint().1.is_some_and(|hi| hi <= len))] + #[ensures(|written| *written <= len && self.len == old(self.len) + *written && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies( + &self.len, + self.slots(dst, cmp::min(len, self.capacity() - dst)), + self.slots(0, len.saturating_sub(self.capacity() - dst)) + ))] unsafe fn write_iter_wrapping( &mut self, dst: usize, @@ -620,7 +769,17 @@ impl VecDeque { /// Frobs the head and tail sections around to handle the fact that we /// just reallocated. Unsafe because it trusts old_capacity. + /// + /// # Safety + /// + /// `old_capacity` must be the capacity the elements were laid out for before the + /// reallocation: `self.len <= old_capacity <= self.capacity()` and `self.head` must be a + /// valid physical index for it (`self.head < old_capacity`, or `0` if it was `0`). #[inline] + #[requires(self.len <= old_capacity && old_capacity <= self.capacity())] + #[requires(self.head < old_capacity || self.head == 0)] + #[ensures(|_| self.len == old(self.len) && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies(&self.head, self.all_slots()))] unsafe fn handle_capacity_increase(&mut self, old_capacity: usize) { let new_capacity = self.capacity(); debug_assert!(new_capacity >= old_capacity); @@ -863,6 +1022,14 @@ impl VecDeque { /// `initialized.start` ≤ `initialized.end` ≤ `capacity`. #[inline] #[cfg(not(test))] + #[requires(initialized.start <= initialized.end && initialized.end <= capacity)] + #[requires(Layout::array::(capacity).is_ok())] + #[requires(T::IS_ZST || capacity == 0 + || core::ub_checks::can_write(ptr::slice_from_raw_parts_mut(ptr, capacity)))] + #[ensures(|result| result.head == old(initialized.start) + && result.len == old(initialized.end) - old(initialized.start) + && result.len <= result.capacity() + && (T::IS_ZST || result.capacity() == capacity))] pub(crate) unsafe fn from_contiguous_raw_parts_in( ptr: *mut T, initialized: Range, @@ -1304,6 +1471,19 @@ impl VecDeque { /// /// `old_head` refers to the head index before `shrink_to` was called. `target_cap` /// is the capacity that it was trying to shrink to. + /// + /// # Safety + /// + /// Must only be called in the state `shrink_to` leaves behind when `buf.shrink_to_fit` + /// unwinds: `self.len <= target_cap <= self.capacity()`, `self.head <= target_cap`, + /// `old_head < self.capacity()`, and either the elements are contiguous within + /// `target_cap` or the head slice `self.head..target_cap` fits back at `old_head`. + #[requires(self.invariant_holds() && self.len <= target_cap && target_cap <= self.capacity())] + #[requires(self.head <= target_cap && old_head < self.capacity())] + #[requires(self.head <= target_cap - self.len + || old_head.checked_add(target_cap - self.head).is_some_and(|end| end <= self.capacity()))] + #[ensures(|_| self.len == old(self.len) && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies(&self.head, self.all_slots()))] unsafe fn abort_shrink(&mut self, old_head: usize, target_cap: usize) { // Moral equivalent of self.head + self.len <= target_cap. Won't overflow // because `self.len <= target_cap`. @@ -2631,6 +2811,8 @@ impl VecDeque { let mut cur = 0; // Stage 1: All values are retained. + #[safety::loop_invariant(cur <= len && idx <= cur)] + #[cfg_attr(kani, kani::loop_modifies(&cur, &idx, self.all_slots()))] while cur < len { if !f(&mut self[cur]) { cur += 1; @@ -2640,6 +2822,8 @@ impl VecDeque { idx += 1; } // Stage 2: Swap retained value into current idx. + #[safety::loop_invariant(cur <= len && idx <= cur)] + #[cfg_attr(kani, kani::loop_modifies(&cur, &idx, self.all_slots()))] while cur < len { if !f(&mut self[cur]) { cur += 1; @@ -2984,6 +3168,9 @@ impl VecDeque { // so it's sound to call here because we're calling with something // less than half the length, which is never above half the capacity. + #[requires(self.invariant_holds() && mid <= self.len / 2)] + #[ensures(|_| self.len == old(self.len) && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies(&self.head, self.all_slots()))] unsafe fn rotate_left_inner(&mut self, mid: usize) { debug_assert!(mid * 2 <= self.len()); unsafe { @@ -2992,6 +3179,9 @@ impl VecDeque { self.head = self.to_physical_idx(mid); } + #[requires(self.invariant_holds() && k <= self.len / 2)] + #[ensures(|_| self.len == old(self.len) && self.invariant_holds())] + #[cfg_attr(kani, kani::modifies(&self.head, self.all_slots()))] unsafe fn rotate_right_inner(&mut self, k: usize) { debug_assert!(k * 2 <= self.len()); self.head = self.wrap_sub(self.head, k); @@ -3768,9 +3958,1144 @@ impl From<[T; N]> for VecDeque { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { - use core::kani; + use core::iter::TrustedLen; + use core::marker::PhantomData; + use core::mem::SizedTypeProperties; + use core::{cmp, kani, ptr}; + use crate::alloc::Layout; use crate::collections::VecDeque; + use crate::vec::Vec; + + /// A non-vacuity witness for a path through the ring buffer. Zero-sized element types never + /// touch the buffer (every such path is excluded by `T::IS_ZST` checks in the code), so the + /// witness is only meaningful, and only required, for sized `T`. (A macro rather than a + /// function because Kani needs the message to be a literal at the `cover` call site.) + macro_rules! cover_buffer_path { + ($t:ty, $cond:expr, $msg:literal) => { + kani::cover(<$t>::IS_ZST || $cond, $msg) + }; + } + + // --------------------------------------------------------------------------------------- + // Symbolic deque generator + // --------------------------------------------------------------------------------------- + + /// Upper bound, in bytes, on the size of the backing allocation. This is not a bound of + /// the proof: it mirrors CBMC's memory model, whose objects are addressed with + /// `64 - object_bits` offset bits (`--object-bits 12` in `scripts/run-kani.sh`), so a single + /// allocation cannot exceed 2^51 bytes in the model. Every `cap` whose allocation fits the + /// model is explored; the bound only excludes allocations no real machine could back either. + const MAX_ALLOCATION_BYTES: usize = 1 << 48; + + /// Builds an arbitrary `VecDeque` with symbolic capacity, symbolic `head` and symbolic + /// `len`, backed by a real allocation of that capacity. + /// + /// * `cap` is only restricted by the layout precondition `RawVec` itself imposes + /// (`Layout::array::(cap).is_ok()`); there is no length bound. + /// * `head` ranges over every valid physical index and `len` over `0..=cap`, so both the + /// contiguous (`head + len <= cap`) and the wrapped (`head + len > cap`) ring layouts are + /// explored (see the `kani::cover` witnesses). + /// * Exactly the logical range `head..head + len` (wrapping at `cap`) is initialized, with an + /// arbitrary byte pattern; slots outside it stay uninitialized. The element types used by + /// the harnesses have no validity invariant, so any byte pattern is a valid `T`, and no + /// proof depends on the element values. + pub(super) fn any_deque() -> VecDeque { + let requested: usize = kani::any(); + kani::assume(Layout::array::(requested).is_ok()); + kani::assume( + requested + .checked_mul(core::mem::size_of::()) + .is_some_and(|b| b <= MAX_ALLOCATION_BYTES), + ); + let mut deque = VecDeque::::with_capacity(requested); + let cap = deque.capacity(); + let head: usize = if cap == 0 { 0 } else { kani::any_where(|h: &usize| *h < cap) }; + let len: usize = kani::any_where(|l: &usize| *l <= cap); + if !T::IS_ZST && len > 0 { + let fill: u8 = kani::any(); + let head_room = cap - head; + unsafe { + if len <= head_room { + ptr::write_bytes(deque.ptr().add(head), fill, len); + } else { + ptr::write_bytes(deque.ptr().add(head), fill, head_room); + ptr::write_bytes(deque.ptr(), fill, len - head_room); + } + } + } + deque.head = head; + deque.len = len; + kani::cover(len > cap - head, "generator: wrapped ring layout is reachable"); + kani::cover(len > 0 && len <= cap - head, "generator: contiguous layout is reachable"); + kani::cover(len == cap && cap > 1, "generator: full deque is reachable"); + cover_buffer_path!(T, cap == 0, "generator: zero-capacity deque is reachable"); + deque + } + + /// Reads a symbolic logical index of `deque` so that the slot is actually dereferenced + /// after the operation under test. + pub(super) fn touch(deque: &VecDeque) { + let i: usize = kani::any(); + if let Some(elem) = deque.get(i) { + let _ = unsafe { ptr::read(elem) }; + } + assert!(deque.invariant_holds()); + } + + /// A harness iterator yielding exactly `remaining` arbitrary elements. It carries no + /// references, so loop-contract havocking cannot invalidate it, and its `size_hint` is + /// exact (it is `TrustedLen`, like every iterator the real callers of `write_iter` pass). + pub(super) struct AnyIter { + remaining: usize, + _marker: PhantomData, + } + + impl AnyIter { + pub(super) fn new(remaining: usize) -> Self { + AnyIter { remaining, _marker: PhantomData } + } + } + + impl Iterator for AnyIter { + type Item = T; + + fn next(&mut self) -> Option { + if self.remaining == 0 { + None + } else { + self.remaining -= 1; + Some(kani::any()) + } + } + + fn size_hint(&self) -> (usize, Option) { + (self.remaining, Some(self.remaining)) + } + + fn advance_by(&mut self, n: usize) -> Result<(), core::num::NonZero> { + let skipped = cmp::min(n, self.remaining); + self.remaining -= skipped; + core::num::NonZero::new(n - skipped).map_or(Ok(()), Err) + } + } + + impl ExactSizeIterator for AnyIter {} + unsafe impl TrustedLen for AnyIter {} + + // --------------------------------------------------------------------------------------- + // Contract harnesses (`proof_for_contract`) for the unsafe functions + // --------------------------------------------------------------------------------------- + + /// Contract replacement for the loop of `VecDeque::write_iter` (`write_iter_loop`), used + /// when verifying the callers of `write_iter` (`write_iter_wrapping`, `resize_with`). + /// `write_iter` itself, loop included, is verified against its real body by + /// `check_write_iter_*`. + /// + /// This is what `#[kani::stub_verified(write_iter)]` would generate. It is written by hand + /// because the pinned Kani (a) cannot generate the replacement of a contract whose + /// `modifies` clause names a slice (kani-compiler `transform/contracts.rs` resolves + /// `write_any_slice` with the slice type itself as the element type and ICEs in + /// `reachability.rs`), and (b) cannot `kani::stub` a function that carries a contract + /// (model-checking/kani#4591); hence the contract-free helper is the stub target. + /// + /// It *asserts* the precondition of `write_iter`'s contract (so a caller violating it fails + /// its proof), then models every behaviour the contract permits: the iterator yields some + /// `n <= hi` elements, exactly the slots `dst..dst + n` receive arbitrary values, and + /// `*written` grows by `n`. The iterator is dropped rather than driven, so no loop is needed. + unsafe fn stub_write_iter_loop( + deque: &mut VecDeque, + dst: usize, + mut iter: impl Iterator, + written: &mut usize, + ) { + let n = unsafe { model_write_iter(deque, dst, &iter, written) }; + // Consume the elements from the iterator exactly as the real loop does, so that an + // iterator shared with a later call (`write_iter_wrapping`'s wrapping branch borrows + // `iter` for the first call and passes it on to the second) reports the right + // remaining length. `advance_by` is O(1) for the harness iterator and the `Take` / + // `ByRefSized` adapters the callee wraps it in. + assert!(iter.advance_by(n).is_ok()); + } + + /// Like [`stub_write_iter_loop`] but drops the iterator instead of advancing it. Only valid + /// where the iterator is not observed after the call, i.e. in the non-wrapping branch of + /// `write_iter_wrapping` (used by the `resize_with` harnesses, whose `Take>` + /// iterator cannot be advanced without a loop). + unsafe fn stub_write_iter_loop_drop( + deque: &mut VecDeque, + dst: usize, + iter: impl Iterator, + written: &mut usize, + ) { + let _ = unsafe { model_write_iter(deque, dst, &iter, written) }; + drop(iter); + } + + /// Shared model of one `write_iter` call: checks the contract's precondition, requires the + /// exact size hint every `TrustedLen` caller guarantees, havocs exactly the slots that + /// receive elements and advances `*written`. Returns the number of elements written. + unsafe fn model_write_iter( + deque: &mut VecDeque, + dst: usize, + iter: &impl Iterator, + written: &mut usize, + ) -> usize { + let (lo, hi) = iter.size_hint(); + let hi = hi.expect("write_iter: iterator must have an upper size bound"); + assert!(lo == hi, "write_iter callers pass TrustedLen iterators"); + assert!(dst.checked_add(hi).is_some_and(|end| end <= deque.capacity())); + assert!(written.checked_add(hi).is_some()); + if !T::IS_ZST && hi > 0 { + unsafe { ptr::write_bytes(deque.ptr().add(dst), kani::any::(), hi) }; + } + *written += hi; + hi + } + + fn check_write_iter() { + let mut deque = any_deque::(); + let dst: usize = kani::any(); + let n: usize = kani::any(); + let mut written: usize = kani::any(); + let before = written; + unsafe { deque.write_iter(dst, AnyIter::::new(n), &mut written) }; + assert_eq!(written, before + n); + kani::cover(n > 1, "write_iter: more than one element written"); + kani::cover(dst > 0 && n > 0, "write_iter: non-zero destination"); + } + + fn check_write_iter_wrapping() { + let mut deque = any_deque::(); + let dst: usize = kani::any(); + let len: usize = kani::any(); + let n: usize = kani::any(); + let old_len = deque.len; + let written = unsafe { deque.write_iter_wrapping(dst, AnyIter::::new(n), len) }; + assert!(written <= len); + assert_eq!(deque.len, old_len + written); + kani::cover(len > deque.capacity() - dst, "write_iter_wrapping: wrapping branch"); + kani::cover(n > 0 && len <= deque.capacity() - dst, "write_iter_wrapping: direct branch"); + touch(&deque); + } + + fn check_copy() { + let mut deque = any_deque::(); + let src: usize = kani::any(); + let dst: usize = kani::any(); + let len: usize = kani::any(); + unsafe { deque.copy(src, dst, len) }; + kani::cover(len > 1 && src.abs_diff(dst) < len, "copy: overlapping ranges"); + kani::cover(len > 1 && src.abs_diff(dst) >= len, "copy: disjoint ranges"); + touch(&deque); + } + + fn check_copy_nonoverlapping() { + let mut deque = any_deque::(); + let src: usize = kani::any(); + let dst: usize = kani::any(); + let len: usize = kani::any(); + unsafe { deque.copy_nonoverlapping(src, dst, len) }; + kani::cover(len > 1, "copy_nonoverlapping: more than one element"); + touch(&deque); + } + + fn check_wrap_copy() { + let mut deque = any_deque::(); + let src: usize = kani::any(); + let dst: usize = kani::any(); + let len: usize = kani::any(); + let cap = deque.capacity(); + unsafe { deque.wrap_copy(src, dst, len) }; + let copying = !T::IS_ZST && cap > 0 && len > 0 && src != dst; + let dst_after_src = copying && deque.wrap_sub(dst, src) < len; + let src_wraps = copying && cap - src < len; + let dst_wraps = copying && cap - dst < len; + cover_buffer_path!(T, copying && !src_wraps && !dst_wraps, "wrap_copy: (_, false, false)"); + cover_buffer_path!( + T, + !dst_after_src && !src_wraps && dst_wraps, + "wrap_copy: (false, false, true)" + ); + cover_buffer_path!( + T, + dst_after_src && !src_wraps && dst_wraps, + "wrap_copy: (true, false, true)" + ); + cover_buffer_path!( + T, + !dst_after_src && src_wraps && !dst_wraps, + "wrap_copy: (false, true, false)" + ); + cover_buffer_path!( + T, + dst_after_src && src_wraps && !dst_wraps, + "wrap_copy: (true, true, false)" + ); + cover_buffer_path!( + T, + !dst_after_src && src_wraps && dst_wraps, + "wrap_copy: (false, true, true)" + ); + cover_buffer_path!( + T, + dst_after_src && src_wraps && dst_wraps, + "wrap_copy: (true, true, true)" + ); + touch(&deque); + } + + fn check_buffer_read() { + let mut deque = any_deque::(); + let off: usize = kani::any(); + let value = unsafe { deque.buffer_read(off) }; + core::mem::forget(value); + kani::cover(off > 0, "buffer_read: non-zero offset"); + } + + fn check_buffer_write() { + let mut deque = any_deque::(); + let off: usize = kani::any(); + let slot = unsafe { deque.buffer_write(off, kani::any()) }; + let _ = unsafe { ptr::read(slot) }; + kani::cover(off > 0, "buffer_write: non-zero offset"); + } + + fn check_push_unchecked() { + let mut deque = any_deque::(); + let old_len = deque.len; + unsafe { deque.push_unchecked(kani::any()) }; + assert_eq!(deque.len, old_len + 1); + kani::cover(old_len >= deque.capacity() - deque.head, "push_unchecked: wrapped write"); + touch(&deque); + } + + // --------------------------------------------------------------------------------------- + // Safe-abstraction harnesses (`kani::proof`) + // --------------------------------------------------------------------------------------- + + /// Abstraction of the *safe* `core::slice::rotate::ptr_rotate` used by + /// `<[T]>::rotate_left/right`: it checks the callee's documented precondition (the range + /// `mid - left .. mid + right` must be valid for reading and writing) and otherwise leaves + /// memory untouched. `make_contiguous` performs no value-dependent operation after the + /// rotation, and a rotation of a valid slice can only permute valid values, so this + /// abstraction is sound for the memory-safety proof of `make_contiguous`. + unsafe fn stub_ptr_rotate(left: usize, mid: *mut T, right: usize) { + let len = left.checked_add(right).expect("rotate range overflows"); + let start = unsafe { mid.sub(left) }; + assert!(core::ub_checks::can_write(ptr::slice_from_raw_parts_mut(start, len))); + } + + fn check_make_contiguous() { + let mut deque = any_deque::(); + let len = deque.len; + let cap = deque.capacity(); + let head = deque.head; + let wrapped = !T::IS_ZST && len > cap - head; + let free = cap - len; + let slice = deque.make_contiguous(); + assert_eq!(slice.len(), len); + if len > 0 { + let _ = unsafe { ptr::read(&slice[len - 1]) }; + } + assert!(deque.is_contiguous()); + let head_len = cap - head; + let tail_len = len.wrapping_sub(head_len); + cover_buffer_path!( + T, + wrapped && free >= head_len, + "make_contiguous: head fits in free space" + ); + cover_buffer_path!( + T, + wrapped && free < head_len && free >= tail_len, + "make_contiguous: tail fits" + ); + cover_buffer_path!( + T, + wrapped && free < head_len && free < tail_len && head_len > tail_len, + "make_contiguous: rotate_left" + ); + cover_buffer_path!( + T, + wrapped && free < head_len && free < tail_len && head_len <= tail_len, + "make_contiguous: rotate_right" + ); + touch(&deque); + } + + // --------------------------------------------------------------------------------------- + // Remaining contract harnesses + // --------------------------------------------------------------------------------------- + + /// Allocates a deque with symbolic capacity and no elements (`head == len == 0`). + pub(super) fn any_empty_deque() -> VecDeque { + let requested: usize = kani::any(); + kani::assume(Layout::array::(requested).is_ok()); + kani::assume( + requested + .checked_mul(core::mem::size_of::()) + .is_some_and(|b| b <= MAX_ALLOCATION_BYTES), + ); + VecDeque::::with_capacity(requested) + } + + /// Lays out a logical ring of `len` elements starting at `head` inside the first `ring_cap` + /// slots of `deque`'s buffer (`ring_cap <= deque.capacity()`, `head < ring_cap` unless + /// `ring_cap == 0`, `len <= ring_cap`): initializes exactly those slots and sets the fields. + pub(super) fn init_ring(deque: &mut VecDeque, ring_cap: usize, head: usize, len: usize) { + assert!(ring_cap <= deque.capacity() && len <= ring_cap); + assert!(head < ring_cap || (ring_cap == 0 && head == 0)); + if !T::IS_ZST && len > 0 { + let fill: u8 = kani::any(); + let head_room = ring_cap - head; + unsafe { + if len <= head_room { + ptr::write_bytes(deque.ptr().add(head), fill, len); + } else { + ptr::write_bytes(deque.ptr().add(head), fill, head_room); + ptr::write_bytes(deque.ptr(), fill, len - head_room); + } + } + } + deque.head = head; + deque.len = len; + } + + /// A `Vec` of symbolic length whose elements are all initialized. + pub(super) fn any_vec() -> Vec { + let len: usize = kani::any(); + kani::assume(Layout::array::(len).is_ok()); + kani::assume( + len.checked_mul(core::mem::size_of::()).is_some_and(|b| b <= MAX_ALLOCATION_BYTES), + ); + let mut vec = Vec::::with_capacity(len); + if !T::IS_ZST && len > 0 { + unsafe { ptr::write_bytes(vec.as_mut_ptr(), kani::any::(), len) }; + } + unsafe { vec.set_len(len) }; + vec + } + + fn check_buffer_range() { + let deque = any_deque::(); + let start: usize = kani::any(); + let end: usize = kani::any(); + let slice = unsafe { deque.buffer_range(start..end) }; + assert_eq!(slice.len(), end - start); + assert!(core::ptr::eq(slice as *const T, unsafe { deque.ptr().add(start) })); + kani::cover(end - start > 1, "buffer_range: more than one slot"); + // `Drop for VecDeque` calls `buffer_range` too; a contract harness must contain a single + // call to the function under contract, so the (element-free) deque is leaked instead. + core::mem::forget(deque); + } + + fn check_copy_slice() { + let mut deque = any_deque::(); + let src = any_vec::(); + let dst: usize = kani::any(); + unsafe { deque.copy_slice(dst, &src) }; + kani::cover(src.len() > 0 && src.len() <= deque.capacity() - dst, "copy_slice: no wrap"); + kani::cover(src.len() > deque.capacity() - dst, "copy_slice: wrapping copy"); + touch(&deque); + } + + fn check_handle_capacity_increase() { + let mut deque = any_empty_deque::(); + let new_cap = deque.capacity(); + let old_cap: usize = kani::any_where(|c: &usize| *c <= new_cap); + let head: usize = if old_cap == 0 { 0 } else { kani::any_where(|h: &usize| *h < old_cap) }; + let len: usize = kani::any_where(|l: &usize| *l <= old_cap); + init_ring(&mut deque, old_cap, head, len); + let contiguous = head <= old_cap - len; + let head_len = old_cap - head; + let case_b = + !contiguous && head_len > len - head_len && new_cap - old_cap >= len - head_len; + unsafe { deque.handle_capacity_increase(old_cap) }; + assert!(deque.is_contiguous() || T::IS_ZST || len > old_cap - head); + kani::cover(contiguous && len > 0, "handle_capacity_increase: case A (no move)"); + kani::cover(case_b, "handle_capacity_increase: case B (tail moved)"); + kani::cover(!contiguous && !case_b, "handle_capacity_increase: case C (head moved)"); + kani::cover(old_cap == 0, "handle_capacity_increase: from zero capacity"); + touch(&deque); + } + + fn check_from_contiguous_raw_parts_in() { + let vec = any_empty_deque_vec::(); + let (ptr, _, capacity, alloc) = vec.into_raw_parts_with_alloc(); + let start: usize = kani::any(); + let end: usize = kani::any(); + if !T::IS_ZST && start <= end && end <= capacity && end > start { + unsafe { ptr::write_bytes(ptr.add(start), kani::any::(), end - start) }; + } + let deque = + unsafe { VecDeque::from_contiguous_raw_parts_in(ptr, start..end, capacity, alloc) }; + assert_eq!(deque.len(), end - start); + let i: usize = kani::any(); + if let Some(elem) = deque.get(i) { + let _ = unsafe { ptr::read(elem) }; + } + // Note: an exhausted `vec::IntoIter` hands over `initialized == capacity..capacity`, so + // `head == capacity` (with `len == 0`) is a state this constructor legitimately + // produces even though the field comments describe `head < capacity`; `wrap_index` + // maps it onto `head == 0`. + kani::cover(end - start > 1 && start > 0, "from_contiguous_raw_parts_in: interior range"); + kani::cover( + start == capacity && capacity > 0, + "from_contiguous_raw_parts_in: head == capacity", + ); + } + + /// A `Vec` with symbolic capacity and no elements, used to obtain raw parts. + fn any_empty_deque_vec() -> Vec { + let requested: usize = kani::any(); + kani::assume(Layout::array::(requested).is_ok()); + kani::assume( + requested + .checked_mul(core::mem::size_of::()) + .is_some_and(|b| b <= MAX_ALLOCATION_BYTES), + ); + Vec::::with_capacity(requested) + } + + fn check_abort_shrink() { + let mut deque = any_empty_deque::(); + let cap = deque.capacity(); + let target_cap: usize = kani::any_where(|c: &usize| *c <= cap); + let len: usize = kani::any_where(|l: &usize| *l <= target_cap); + let head: usize = kani::any_where(|h: &usize| *h <= target_cap); + let old_head: usize = kani::any_where(|h: &usize| *h < cap); + kani::assume(head < target_cap || len == 0); + if head < target_cap { + init_ring(&mut deque, target_cap, head, len); + } else { + deque.head = head; + deque.len = 0; + } + let contiguous = head <= target_cap - len; + let head_len = target_cap - head; + let tail_len = len.wrapping_sub(head_len); + let case_b = !contiguous && tail_len <= cmp::min(head_len, cap - target_cap); + unsafe { deque.abort_shrink(old_head, target_cap) }; + kani::cover(contiguous && len > 0, "abort_shrink: contiguous, nothing to do"); + kani::cover(case_b, "abort_shrink: tail copied to the back"); + kani::cover(!contiguous && !case_b, "abort_shrink: head copied back to old_head"); + touch(&deque); + } + + fn check_rotate_left_inner() { + let mut deque = any_deque::(); + let mid: usize = kani::any(); + unsafe { deque.rotate_left_inner(mid) }; + kani::cover(mid > 1, "rotate_left_inner: rotation by more than one"); + touch(&deque); + } + + fn check_rotate_right_inner() { + let mut deque = any_deque::(); + let k: usize = kani::any(); + unsafe { deque.rotate_right_inner(k) }; + kani::cover(k > 1, "rotate_right_inner: rotation by more than one"); + touch(&deque); + } + + // --------------------------------------------------------------------------------------- + // Safe-abstraction harnesses + // --------------------------------------------------------------------------------------- + + /// `push_*`, `insert`, `reserve*` and `append` may legitimately panic with "capacity + /// overflow" when the requested capacity cannot be represented; the harnesses assume the + /// documented non-panicking condition instead (the new capacity fits the allocation model). + fn assume_can_grow_by(deque: &VecDeque, additional: usize) { + kani::assume(deque.len().checked_add(additional).is_some_and(|new_len| { + new_len + .checked_mul(core::mem::size_of::()) + .is_some_and(|b| b <= MAX_ALLOCATION_BYTES) + && (!T::IS_ZST || new_len < usize::MAX) + })); + } + + fn check_get() { + let deque = any_deque::(); + let i: usize = kani::any(); + let elem = deque.get(i); + assert_eq!(elem.is_some(), i < deque.len()); + if let Some(elem) = elem { + let _ = unsafe { ptr::read(elem) }; + } + kani::cover(i > 0 && i < deque.len(), "get: in-bounds non-front index"); + kani::cover(i >= deque.len(), "get: out-of-bounds index"); + } + + fn check_get_mut() { + let mut deque = any_deque::(); + let i: usize = kani::any(); + let len = deque.len(); + let elem = deque.get_mut(i); + assert_eq!(elem.is_some(), i < len); + if let Some(elem) = elem { + *elem = kani::any(); + } + kani::cover(i > 0 && i < len, "get_mut: in-bounds non-front index"); + touch(&deque); + } + + fn check_swap() { + let mut deque = any_deque::(); + let len = deque.len(); + let i: usize = kani::any_where(|x: &usize| *x < len); + let j: usize = kani::any_where(|x: &usize| *x < len); + deque.swap(i, j); + kani::cover(i != j, "swap: distinct indices"); + touch(&deque); + } + + fn check_as_slices() { + let deque = any_deque::(); + let (a, b) = deque.as_slices(); + assert_eq!(a.len() + b.len(), deque.len()); + if let Some(last) = a.last() { + let _ = unsafe { ptr::read(last) }; + } + if let Some(last) = b.last() { + let _ = unsafe { ptr::read(last) }; + } + kani::cover(!a.is_empty() && !b.is_empty(), "as_slices: both halves non-empty"); + } + + fn check_as_mut_slices() { + let mut deque = any_deque::(); + let len = deque.len(); + let (a, b) = deque.as_mut_slices(); + assert_eq!(a.len() + b.len(), len); + if let Some(last) = a.last_mut() { + *last = kani::any(); + } + if let Some(first) = b.first_mut() { + *first = kani::any(); + } + kani::cover(!a.is_empty() && !b.is_empty(), "as_mut_slices: both halves non-empty"); + touch(&deque); + } + + fn any_subrange(len: usize) -> (usize, usize) { + let start: usize = kani::any_where(|s: &usize| *s <= len); + let end: usize = kani::any_where(|e: &usize| *e >= start && *e <= len); + (start, end) + } + + fn check_range() { + let deque = any_deque::(); + let (start, end) = any_subrange(deque.len()); + let mut iter = deque.range(start..end); + assert_eq!(iter.len(), end - start); + if let Some(first) = iter.next() { + let _ = unsafe { ptr::read(first) }; + } + if let Some(last) = iter.next_back() { + let _ = unsafe { ptr::read(last) }; + } + kani::cover(end - start > 2, "range: more than two elements"); + } + + fn check_range_mut() { + let mut deque = any_deque::(); + let (start, end) = any_subrange(deque.len()); + let mut iter = deque.range_mut(start..end); + assert_eq!(iter.len(), end - start); + if let Some(first) = iter.next() { + *first = kani::any(); + } + if let Some(last) = iter.next_back() { + *last = kani::any(); + } + kani::cover(end - start > 2, "range_mut: more than two elements"); + touch(&deque); + } + + fn check_drain() { + let mut deque = any_deque::(); + let len = deque.len(); + let (start, end) = any_subrange(len); + let mut drain = deque.drain(start..end); + let pull_front: bool = kani::any(); + let pull_back: bool = kani::any(); + if pull_front { + if let Some(elem) = drain.next() { + core::mem::forget(elem); + } + } + if pull_back { + if let Some(elem) = drain.next_back() { + core::mem::forget(elem); + } + } + drop(drain); + assert_eq!(deque.len(), len - (end - start)); + kani::cover( + start > 0 && end < len && end > start, + "drain: interior range (elements moved)", + ); + kani::cover(start == 0 && end == len && len > 0, "drain: everything drained"); + kani::cover(start > 0 && end == len && end > start, "drain: tail drained"); + kani::cover(start == 0 && end < len && end > 0, "drain: head drained"); + touch(&deque); + } + + fn check_pop_front() { + let mut deque = any_deque::(); + let len = deque.len(); + let elem = deque.pop_front(); + assert_eq!(elem.is_some(), len > 0); + assert_eq!(deque.len(), len.saturating_sub(1)); + core::mem::forget(elem); + kani::cover(len > 1, "pop_front: elements remain"); + touch(&deque); + } + + fn check_pop_back() { + let mut deque = any_deque::(); + let len = deque.len(); + let elem = deque.pop_back(); + assert_eq!(elem.is_some(), len > 0); + assert_eq!(deque.len(), len.saturating_sub(1)); + core::mem::forget(elem); + kani::cover(len > 1, "pop_back: elements remain"); + touch(&deque); + } + + fn check_push_front() { + let mut deque = any_deque::(); + let len = deque.len(); + let full = deque.is_full(); + assume_can_grow_by(&deque, 1); + deque.push_front(kani::any()); + assert_eq!(deque.len(), len + 1); + cover_buffer_path!(T, full && len > 0, "push_front: buffer grown"); + kani::cover(!full && len > 0, "push_front: no growth"); + touch(&deque); + } + + fn check_push_back() { + let mut deque = any_deque::(); + let len = deque.len(); + let full = deque.is_full(); + assume_can_grow_by(&deque, 1); + deque.push_back(kani::any()); + assert_eq!(deque.len(), len + 1); + cover_buffer_path!(T, full && len > 0, "push_back: buffer grown"); + kani::cover(!full && len > 0, "push_back: no growth"); + touch(&deque); + } + + fn check_reserve() { + let mut deque = any_deque::(); + let len = deque.len(); + let old_cap = deque.capacity(); + let additional: usize = kani::any(); + assume_can_grow_by(&deque, additional); + deque.reserve(additional); + assert_eq!(deque.len(), len); + assert!(deque.capacity() >= len + additional); + cover_buffer_path!(T, len + additional > old_cap && len > 0, "reserve: buffer grown"); + kani::cover(len + additional <= old_cap, "reserve: no growth"); + touch(&deque); + } + + fn check_reserve_exact() { + let mut deque = any_deque::(); + let len = deque.len(); + let old_cap = deque.capacity(); + let additional: usize = kani::any(); + assume_can_grow_by(&deque, additional); + deque.reserve_exact(additional); + assert_eq!(deque.len(), len); + assert!(deque.capacity() >= len + additional); + cover_buffer_path!(T, len + additional > old_cap && len > 0, "reserve_exact: buffer grown"); + kani::cover(len + additional <= old_cap, "reserve_exact: no growth"); + touch(&deque); + } + + fn check_try_reserve() { + let mut deque = any_deque::(); + let len = deque.len(); + let old_cap = deque.capacity(); + let additional: usize = kani::any(); + let result = deque.try_reserve(additional); + assert_eq!(deque.len(), len); + if result.is_ok() { + assert!(deque.capacity() >= len + additional); + } + cover_buffer_path!( + T, + result.is_ok() && len + additional > old_cap && len > 0, + "try_reserve: buffer grown" + ); + kani::cover(result.is_err(), "try_reserve: capacity overflow reported"); + touch(&deque); + } + + fn check_try_reserve_exact() { + let mut deque = any_deque::(); + let len = deque.len(); + let old_cap = deque.capacity(); + let additional: usize = kani::any(); + let result = deque.try_reserve_exact(additional); + assert_eq!(deque.len(), len); + if result.is_ok() { + assert!(deque.capacity() >= len + additional); + } + cover_buffer_path!( + T, + result.is_ok() && len + additional > old_cap && len > 0, + "try_reserve_exact: buffer grown" + ); + kani::cover(result.is_err(), "try_reserve_exact: capacity overflow reported"); + touch(&deque); + } + + fn check_shrink_to() { + let mut deque = any_deque::(); + let len = deque.len(); + let head = deque.head; + let cap = deque.capacity(); + let min_capacity: usize = kani::any(); + let target_cap = cmp::max(min_capacity, len); + let end = head as u128 + len as u128; + let tail_outside = target_cap < cap && end > target_cap as u128 && end <= cap as u128; + deque.shrink_to(min_capacity); + assert_eq!(deque.len(), len); + assert!(deque.capacity() >= cmp::min(target_cap, cap)); + let shrinking = !T::IS_ZST && target_cap < cap && len > 0; + cover_buffer_path!( + T, + shrinking && head >= target_cap && tail_outside, + "shrink_to: all elements moved to front" + ); + cover_buffer_path!( + T, + shrinking && head < target_cap && tail_outside, + "shrink_to: tail wrapped to front" + ); + cover_buffer_path!( + T, + shrinking && !tail_outside && end > cap as u128, + "shrink_to: head slice moved back" + ); + cover_buffer_path!( + T, + shrinking && !tail_outside && end <= target_cap as u128, + "shrink_to: elements untouched" + ); + touch(&deque); + } + + fn check_truncate() { + let mut deque = any_deque::(); + let len = deque.len(); + let front_len = deque.as_slices().0.len(); + let new_len: usize = kani::any(); + deque.truncate(new_len); + assert_eq!(deque.len(), cmp::min(len, new_len)); + kani::cover(new_len < len && new_len > front_len, "truncate: cut inside the back slice"); + kani::cover( + new_len < len && new_len <= front_len && front_len < len, + "truncate: cut inside the front slice, back dropped", + ); + kani::cover(new_len >= len, "truncate: no-op"); + touch(&deque); + } + + fn check_insert() { + let mut deque = any_deque::(); + let len = deque.len(); + let full = deque.is_full(); + let index: usize = kani::any_where(|i: &usize| *i <= len); + assume_can_grow_by(&deque, 1); + deque.insert(index, kani::any()); + assert_eq!(deque.len(), len + 1); + kani::cover(len - index < index, "insert: back half shifted"); + kani::cover(len - index >= index && index > 0, "insert: front half shifted"); + cover_buffer_path!(T, full && len > 0, "insert: buffer grown"); + touch(&deque); + } + + fn check_remove() { + let mut deque = any_deque::(); + let len = deque.len(); + let index: usize = kani::any(); + let elem = deque.remove(index); + assert_eq!(elem.is_some(), index < len); + assert_eq!(deque.len(), if index < len { len - 1 } else { len }); + core::mem::forget(elem); + kani::cover(index < len && len - index - 1 < index, "remove: back half shifted"); + kani::cover( + index < len && len - index - 1 >= index && index > 0, + "remove: front half shifted", + ); + touch(&deque); + } + + fn check_split_off() { + let mut deque = any_deque::(); + let len = deque.len(); + let first_len = deque.as_slices().0.len(); + let at: usize = kani::any_where(|a: &usize| *a <= len); + let other = deque.split_off(at); + assert_eq!(deque.len(), at); + assert_eq!(other.len(), len - at); + kani::cover(at < first_len && first_len < len, "split_off: split inside the first half"); + kani::cover( + at >= first_len && at < len && first_len < len, + "split_off: split inside the second half", + ); + touch(&deque); + touch(&other); + } + + fn check_append() { + let mut deque = any_deque::(); + let mut other = any_deque::(); + let len = deque.len(); + let other_len = other.len(); + let old_cap = deque.capacity(); + assume_can_grow_by(&deque, other_len); + deque.append(&mut other); + assert_eq!(deque.len(), len + other_len); + assert_eq!(other.len(), 0); + cover_buffer_path!(T, len + other_len > old_cap && other_len > 0, "append: buffer grown"); + kani::cover(len + other_len <= old_cap && other_len > 0 && len > 0, "append: in place"); + touch(&deque); + touch(&other); + } + + fn check_retain_mut() { + let mut deque = any_deque::(); + let len = deque.len(); + deque.retain_mut(|elem| { + let keep: bool = kani::any(); + if keep { + *elem = kani::any(); + } + keep + }); + assert!(deque.len() <= len); + kani::cover(deque.len() > 0 && deque.len() < len, "retain_mut: some elements removed"); + touch(&deque); + } + + fn check_grow() { + let mut deque = any_deque::(); + kani::assume(deque.is_full()); + let len = deque.len(); + assume_can_grow_by(&deque, 1); + deque.grow(); + assert_eq!(deque.len(), len); + assert!(!deque.is_full()); + kani::cover(len > 1, "grow: non-trivial deque"); + touch(&deque); + } + + /// `resize_with` appends through `extend` → `write_iter_wrapping` with a + /// `Take>` iterator. That iterator cannot be advanced without a loop, so the + /// contract replacement of `write_iter`'s loop can only model calls after which the + /// iterator is not reused, i.e. the non-wrapping branch of `write_iter_wrapping` (see + /// `stub_write_iter_loop_drop`). The two `resize_with` harnesses therefore restrict the + /// appended elements to not wrap around the end of the buffer, in two complementary ways; + /// the wrapping write path itself is verified by `check_write_iter_wrapping_*`. + /// + /// Variant 1: arbitrary (possibly wrapped) deque, capacity reserved up front so that the + /// appended elements fit behind the last element without wrapping. + fn check_resize_with() { + let mut deque = any_deque::(); + let len = deque.len(); + let new_len: usize = kani::any(); + if new_len > len { + let additional = new_len - len; + assume_can_grow_by(&deque, additional); + deque.reserve(additional); + kani::assume(additional <= deque.capacity() - deque.to_physical_idx(len)); + } + deque.resize_with(new_len, || kani::any()); + assert_eq!(deque.len(), new_len); + kani::cover( + new_len > len && new_len - len > 1 && len > 0 && deque.head > 0, + "resize_with: grown by more than one", + ); + kani::cover(new_len < len, "resize_with: truncated"); + touch(&deque); + } + + /// Variant 2: contiguous deque starting at `head == 0`, so that the growth performed by + /// `resize_with` itself (`reserve` → `handle_capacity_increase`, case A) keeps the appended + /// elements from wrapping. + fn check_resize_with_grow() { + let mut deque = any_deque::(); + kani::assume(deque.head == 0); + let len = deque.len(); + let cap = deque.capacity(); + let new_len: usize = kani::any(); + if new_len > len { + assume_can_grow_by(&deque, new_len - len); + } + deque.resize_with(new_len, || kani::any()); + assert_eq!(deque.len(), new_len); + cover_buffer_path!(T, new_len > cap && len > 0, "resize_with: buffer grown"); + kani::cover( + new_len > len && new_len - len > 1 && new_len <= cap, + "resize_with: appended in place", + ); + touch(&deque); + } + + fn check_rotate_left() { + let mut deque = any_deque::(); + let len = deque.len(); + let n: usize = kani::any_where(|n: &usize| *n <= len); + deque.rotate_left(n); + assert_eq!(deque.len(), len); + kani::cover(n > 0 && n <= len - n, "rotate_left: via rotate_left_inner"); + kani::cover(n > len - n, "rotate_left: via rotate_right_inner"); + touch(&deque); + } + + fn check_rotate_right() { + let mut deque = any_deque::(); + let len = deque.len(); + let n: usize = kani::any_where(|n: &usize| *n <= len); + deque.rotate_right(n); + assert_eq!(deque.len(), len); + kani::cover(n > 0 && n <= len - n, "rotate_right: via rotate_right_inner"); + kani::cover(n > len - n, "rotate_right: via rotate_left_inner"); + touch(&deque); + } + + // --------------------------------------------------------------------------------------- + // Instantiation over element types. + // --------------------------------------------------------------------------------------- + + macro_rules! contract_harness { + ($target:ident, $harness:ident, $ty:ty, $name:ident, [$($attr:meta),*]) => { + #[kani::proof_for_contract(VecDeque::<$ty>::$target)] + $(#[$attr])* + fn $name() { + $harness::<$ty>(); + } + }; + } + + macro_rules! contract_harnesses { + ($target:ident, $harness:ident, [$($ty:ty => $name:ident),* $(,)?]) => { + $( contract_harness!($target, $harness, $ty, $name, []); )* + }; + ($target:ident, $harness:ident, $attrs:tt, [$($ty:ty => $name:ident),* $(,)?]) => { + $( contract_harness!($target, $harness, $ty, $name, $attrs); )* + }; + } + + macro_rules! proof_harness { + ($harness:ident, $ty:ty, $name:ident, [$($attr:meta),*]) => { + #[kani::proof] + $(#[$attr])* + fn $name() { + $harness::<$ty>(); + } + }; + } + + macro_rules! proof_harnesses { + ($harness:ident, $attrs:tt, [$($ty:ty => $name:ident),* $(,)?]) => { + $( proof_harness!($harness, $ty, $name, $attrs); )* + }; + } + + contract_harnesses!(push_unchecked, check_push_unchecked, [u8 => check_push_unchecked_u8, u64 => check_push_unchecked_u64, [u8; 3] => check_push_unchecked_u8x3, () => check_push_unchecked_unit]); + contract_harnesses!(buffer_read, check_buffer_read, [u8 => check_buffer_read_u8, u64 => check_buffer_read_u64, [u8; 3] => check_buffer_read_u8x3, () => check_buffer_read_unit]); + contract_harnesses!(buffer_write, check_buffer_write, [u8 => check_buffer_write_u8, u64 => check_buffer_write_u64, [u8; 3] => check_buffer_write_u8x3, () => check_buffer_write_unit]); + contract_harnesses!(buffer_range, check_buffer_range, [u8 => check_buffer_range_u8, u64 => check_buffer_range_u64, [u8; 3] => check_buffer_range_u8x3, () => check_buffer_range_unit]); + contract_harnesses!(copy, check_copy, [u8 => check_copy_u8, u64 => check_copy_u64, [u8; 3] => check_copy_u8x3, () => check_copy_unit]); + contract_harnesses!(copy_nonoverlapping, check_copy_nonoverlapping, [u8 => check_copy_nonoverlapping_u8, u64 => check_copy_nonoverlapping_u64, [u8; 3] => check_copy_nonoverlapping_u8x3, () => check_copy_nonoverlapping_unit]); + contract_harnesses!(wrap_copy, check_wrap_copy, [u8 => check_wrap_copy_u8, u64 => check_wrap_copy_u64, () => check_wrap_copy_unit]); + contract_harnesses!(copy_slice, check_copy_slice, [u8 => check_copy_slice_u8, u64 => check_copy_slice_u64, () => check_copy_slice_unit]); + contract_harnesses!(write_iter, check_write_iter, [u8 => check_write_iter_u8, u64 => check_write_iter_u64, [u8; 3] => check_write_iter_u8x3, () => check_write_iter_unit]); + contract_harnesses!( + write_iter_wrapping, + check_write_iter_wrapping, + [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop)], + [u8 => check_write_iter_wrapping_u8] + ); + contract_harnesses!( + write_iter_wrapping, + check_write_iter_wrapping, + [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop)], + [u64 => check_write_iter_wrapping_u64] + ); + contract_harnesses!( + write_iter_wrapping, + check_write_iter_wrapping, + [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop)], + [() => check_write_iter_wrapping_unit] + ); + contract_harnesses!(handle_capacity_increase, check_handle_capacity_increase, [u8 => check_handle_capacity_increase_u8, u64 => check_handle_capacity_increase_u64, () => check_handle_capacity_increase_unit]); + contract_harnesses!(from_contiguous_raw_parts_in, check_from_contiguous_raw_parts_in, [u8 => check_from_contiguous_raw_parts_in_u8, u64 => check_from_contiguous_raw_parts_in_u64, [u8; 3] => check_from_contiguous_raw_parts_in_u8x3, () => check_from_contiguous_raw_parts_in_unit]); + contract_harnesses!(abort_shrink, check_abort_shrink, [u8 => check_abort_shrink_u8, u64 => check_abort_shrink_u64, () => check_abort_shrink_unit]); + contract_harnesses!(rotate_left_inner, check_rotate_left_inner, [u8 => check_rotate_left_inner_u8, u64 => check_rotate_left_inner_u64, () => check_rotate_left_inner_unit]); + contract_harnesses!(rotate_right_inner, check_rotate_right_inner, [u8 => check_rotate_right_inner_u8, u64 => check_rotate_right_inner_u64, () => check_rotate_right_inner_unit]); + + proof_harnesses!(check_get, [], [u8 => check_get_u8, u64 => check_get_u64, () => check_get_unit]); + proof_harnesses!(check_get_mut, [], [u8 => check_get_mut_u8, u64 => check_get_mut_u64, () => check_get_mut_unit]); + proof_harnesses!(check_swap, [], [u8 => check_swap_u8, u64 => check_swap_u64, () => check_swap_unit]); + proof_harnesses!(check_as_slices, [], [u8 => check_as_slices_u8, u64 => check_as_slices_u64, () => check_as_slices_unit]); + proof_harnesses!(check_as_mut_slices, [], [u8 => check_as_mut_slices_u8, u64 => check_as_mut_slices_u64, () => check_as_mut_slices_unit]); + proof_harnesses!(check_range, [], [u8 => check_range_u8, () => check_range_unit]); + proof_harnesses!(check_range_mut, [], [u8 => check_range_mut_u8, () => check_range_mut_unit]); + proof_harnesses!(check_drain, [], [u8 => check_drain_u8, () => check_drain_unit]); + proof_harnesses!(check_pop_front, [], [u8 => check_pop_front_u8, u64 => check_pop_front_u64, () => check_pop_front_unit]); + proof_harnesses!(check_pop_back, [], [u8 => check_pop_back_u8, u64 => check_pop_back_u64, () => check_pop_back_unit]); + proof_harnesses!(check_push_front, [], [u8 => check_push_front_u8, u64 => check_push_front_u64, () => check_push_front_unit]); + proof_harnesses!(check_push_back, [], [u8 => check_push_back_u8, u64 => check_push_back_u64, () => check_push_back_unit]); + proof_harnesses!(check_reserve, [], [u8 => check_reserve_u8, u64 => check_reserve_u64, () => check_reserve_unit]); + proof_harnesses!(check_reserve_exact, [], [u8 => check_reserve_exact_u8, () => check_reserve_exact_unit]); + proof_harnesses!(check_try_reserve, [], [u8 => check_try_reserve_u8, () => check_try_reserve_unit]); + proof_harnesses!(check_try_reserve_exact, [], [u8 => check_try_reserve_exact_u8, u64 => check_try_reserve_exact_u64, () => check_try_reserve_exact_unit]); + proof_harnesses!(check_shrink_to, [], [u8 => check_shrink_to_u8, u64 => check_shrink_to_u64, () => check_shrink_to_unit]); + proof_harnesses!(check_truncate, [], [u8 => check_truncate_u8, u64 => check_truncate_u64, () => check_truncate_unit]); + proof_harnesses!(check_insert, [], [u8 => check_insert_u8, () => check_insert_unit]); + proof_harnesses!(check_remove, [], [u8 => check_remove_u8, () => check_remove_unit]); + proof_harnesses!(check_split_off, [], [u8 => check_split_off_u8, u64 => check_split_off_u64, () => check_split_off_unit]); + proof_harnesses!(check_append, [], [u8 => check_append_u8, () => check_append_unit]); + proof_harnesses!(check_retain_mut, [], [u8 => check_retain_mut_u8, () => check_retain_mut_unit]); + // `grow` is only ever called on a full deque; for a zero-sized `T` that means + // `len == usize::MAX`, where growing panics with "capacity overflow" by design, so there + // is no non-panicking ZST instance to verify. + proof_harnesses!(check_grow, [], [u8 => check_grow_u8]); + proof_harnesses!( + check_resize_with, + [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop_drop)], + [u8 => check_resize_with_u8] + ); + proof_harnesses!( + check_resize_with, + [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop_drop)], + [() => check_resize_with_unit] + ); + proof_harnesses!( + check_resize_with_grow, + [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop_drop)], + [u8 => check_resize_with_grow_u8] + ); + proof_harnesses!( + check_resize_with_grow, + [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop_drop)], + [() => check_resize_with_grow_unit] + ); + proof_harnesses!( + check_make_contiguous, + [kani::stub(core::slice::rotate::ptr_rotate, stub_ptr_rotate)], + [u8 => check_make_contiguous_u8, () => check_make_contiguous_unit] + ); + proof_harnesses!(check_rotate_left, [], [u8 => check_rotate_left_u8, () => check_rotate_left_unit]); + proof_harnesses!(check_rotate_right, [], [u8 => check_rotate_right_u8, () => check_rotate_right_unit]); #[kani::proof] fn check_vecdeque_swap() { diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 9a714e42c14b1..fa3b1e23ba650 100644 --- a/library/alloc/src/lib.rs +++ b/library/alloc/src/lib.rs @@ -183,6 +183,7 @@ #![feature(negative_impls)] #![feature(never_type)] #![feature(optimize_attribute)] +#![feature(proc_macro_hygiene)] #![feature(rustc_allow_const_fn_unstable)] #![feature(rustc_attrs)] #![feature(slice_internals)] From c35ff17ead1d10a35e47f70f12275bec7eaf20d4 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Tue, 8 Sep 2026 18:32:36 +1000 Subject: [PATCH 2/3] Require a valid head in from_contiguous_raw_parts_in's contract `initialized.start == capacity` (an exhausted `vec::IntoIter` whose `Vec` had `capacity == len`) produced a deque with `head == capacity`; `pop_front` reads slot `head` unwrapped, so that state reads past the buffer (rust-lang/rust#162452, I-unsound). The contract now requires `initialized.start < capacity || initialized.start == 0` and ensures the structural invariant, and the harness note no longer calls the state harmless. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_011hQMihqVQLDerCELXExGHg --- .../alloc/src/collections/vec_deque/mod.rs | 27 +++++++++++-------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index f55e9549df798..e67fa5cec01e0 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -1022,13 +1022,20 @@ impl VecDeque { /// `initialized.start` ≤ `initialized.end` ≤ `capacity`. #[inline] #[cfg(not(test))] + /// + /// In addition, `initialized.start` must be a valid `head`, i.e. `initialized.start < + /// capacity` unless the range is `0..0`: the resulting deque uses `head` unwrapped (e.g. + /// `pop_front` reads slot `head` directly), so `head == capacity` reads past the buffer. + /// (`vec::IntoIter::into_vecdeque` currently violates this for an exhausted iterator whose + /// `Vec` had `capacity == len`; see rust-lang/rust#162452.) #[requires(initialized.start <= initialized.end && initialized.end <= capacity)] + #[requires(initialized.start < capacity || initialized.start == 0)] #[requires(Layout::array::(capacity).is_ok())] #[requires(T::IS_ZST || capacity == 0 || core::ub_checks::can_write(ptr::slice_from_raw_parts_mut(ptr, capacity)))] #[ensures(|result| result.head == old(initialized.start) && result.len == old(initialized.end) - old(initialized.start) - && result.len <= result.capacity() + && result.invariant_holds() && (T::IS_ZST || result.capacity() == capacity))] pub(crate) unsafe fn from_contiguous_raw_parts_in( ptr: *mut T, @@ -4431,18 +4438,16 @@ mod verify { let deque = unsafe { VecDeque::from_contiguous_raw_parts_in(ptr, start..end, capacity, alloc) }; assert_eq!(deque.len(), end - start); - let i: usize = kani::any(); - if let Some(elem) = deque.get(i) { - let _ = unsafe { ptr::read(elem) }; - } - // Note: an exhausted `vec::IntoIter` hands over `initialized == capacity..capacity`, so - // `head == capacity` (with `len == 0`) is a state this constructor legitimately - // produces even though the field comments describe `head < capacity`; `wrap_index` - // maps it onto `head == 0`. + // The `initialized.start < capacity || initialized.start == 0` precondition is what + // keeps `head` a valid physical index. Without it, `capacity..capacity` (which + // `vec::IntoIter::into_vecdeque` produces for an exhausted iterator whose `Vec` had + // `capacity == len`) yields `head == capacity`, and a subsequent `push_back` + + // `pop_front` reads one past the end of the buffer: rust-lang/rust#162452. + touch(&deque); kani::cover(end - start > 1 && start > 0, "from_contiguous_raw_parts_in: interior range"); kani::cover( - start == capacity && capacity > 0, - "from_contiguous_raw_parts_in: head == capacity", + start == 0 && end == 0 && capacity > 0, + "from_contiguous_raw_parts_in: empty range", ); } From ee70c8a87959a5476155c8e9e6c1e0c1aab37634 Mon Sep 17 00:00:00 2001 From: Jared Reyes Date: Sun, 13 Sep 2026 17:56:55 +1000 Subject: [PATCH 3/3] Address the Challenge 25 review: shapes, transcription evidence, stub checks Sync with main (toolchain nightly-2026-02-05, Kani 152c6a8, CBMC 6.10.0). At this pin Kani compares a stub's signature with the original's by the position of their own generic parameters, which rejects a free function as the stub of a method; the contract replacement for `write_iter_loop` is therefore a `#[cfg(kani)]` sibling method now. Generic `T`: add the shapes `bool` (validity invariant; generators now write a valid bit pattern of the shape), `Al16` (`repr(align(16))`) and `WithDrop` (`needs_drop`, non-`Copy`, destructor counter) on the targets that exercise them; the slice drop glue is checked bounded for `WithDrop` (`truncate`, `drain`, `retain_mut`, `Drop for VecDeque`); alias drops of bitwise copies in harnesses become `mem::forget`; the module doc states the shape matrix and the parametricity argument. `write_iter` transcription: the shipped `for_each` statement is compiled under Kani byte for byte as `write_iter_for_each` and checked against `write_iter`'s contract with a bounded iterator length; the docs derive why no unbounded proof of the shipped text exists at any current pin and why `stub_verified` (with or without kani#4749) would not discharge the wrapping branch. Stubs: `stub_write_iter_loop`/`model_write_iter` become `VecDeque::write_iter_contract_replacement`, which asserts the contract's own predicate (`write_iter_precondition`) and havocs the `modifies` expression; its one step beyond the contract (consuming the iterator by `hi`) and `stub_ptr_rotate`'s abstraction get bounded checks in `verify::bounded_evidence`, the only place using `kani::unwind`. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01XjuqtSUTkxA5kjmq32PEoJ --- .../alloc/src/collections/vec_deque/mod.rs | 822 +++++++++++++++--- 1 file changed, 678 insertions(+), 144 deletions(-) diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index 04f7379bb313c..666e909e42792 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -656,10 +656,7 @@ impl VecDeque { /// this through the iterator's upper `size_hint`, which is exact for the `TrustedLen` /// iterators every caller passes. #[inline] - #[requires(iter.size_hint().1.is_some_and(|hi| { - dst.checked_add(hi).is_some_and(|end| end <= self.capacity()) - && written.checked_add(hi).is_some() - }))] + #[requires(self.write_iter_precondition(dst, iter.size_hint().1, *written))] #[ensures(|_| old(*written) <= *written && *written - old(*written) <= old(iter.size_hint().1.unwrap_or(0)))] #[cfg_attr(kani, kani::modifies(written, self.slots(dst, iter.size_hint().1.unwrap_or(0))))] @@ -676,20 +673,68 @@ impl VecDeque { }); // Under Kani the very same iteration is spelled as an explicit loop (see // `write_iter_loop`) so that a loop contract can be attached; loop contracts cannot be - // attached to the closure-driven `for_each`. + // attached to the closure-driven `for_each`. The statement above is also compiled + // under Kani, byte for byte, as `write_iter_for_each`, and checked against this + // function's contract for bounded iterator lengths (`verify::bounded_evidence`). #[cfg(kani)] unsafe { self.write_iter_loop(dst, iter, written) } } - /// The loop of [`Self::write_iter`] in the form Kani's loop contracts accept: every element - /// yielded by `iter` is written to `dst + i` and counted, exactly as `for_each` does above; - /// nothing is skipped, synthesized or forgotten. It is verified as part of `write_iter`'s - /// contract proof (`check_write_iter_*` in `mod verify`). Callers of `write_iter` are - /// verified with this helper replaced by its contract (`stub_write_iter_loop`), because a - /// loop contract cannot survive the havocking of the reference-carrying - /// `Take>` adapter that `write_iter_wrapping` passes. + /// The precondition of [`Self::write_iter`]'s contract as one predicate, so that the + /// contract replacement in `mod verify` (`write_iter_contract_replacement`) asserts exactly + /// the clause the contract requires. Only used by the verification contracts and by + /// `mod verify`. + #[cfg(kani)] + fn write_iter_precondition(&self, dst: usize, upper: Option, written: usize) -> bool { + upper.is_some_and(|hi| { + dst.checked_add(hi).is_some_and(|end| end <= self.capacity()) + && written.checked_add(hi).is_some() + }) + } + + /// The shipped statement of [`Self::write_iter`] (its `#[cfg(not(kani))]` body), byte for + /// byte, as a Kani-visible sibling: `verify::bounded_evidence` substitutes it for + /// `write_iter_loop` to check the shipped text against `write_iter`'s contract, bounded in + /// the iterator length. It must stay byte-identical to that statement; diff the two when + /// editing either. + #[cfg(kani)] + #[inline] + unsafe fn write_iter_for_each( + &mut self, + dst: usize, + iter: impl Iterator, + written: &mut usize, + ) { + iter.enumerate().for_each(|(i, element)| unsafe { + self.buffer_write(dst + i, element); + *written += 1; + }); + } + + /// The iteration of [`Self::write_iter`] transcribed into the form Kani's loop contracts + /// accept: `iter` is driven with `next()`, every element is written to `dst + i` and + /// counted, exactly as the shipped `for_each` statement does; nothing is skipped, + /// synthesized or forgotten. `write_iter`'s contract proof (`check_write_iter_*` in + /// `mod verify`) runs this transcription unbounded; `verify::bounded_evidence` checks the + /// shipped statement itself ([`Self::write_iter_for_each`]) against the same contract, + /// bounded in the iterator length. + /// + /// Why a transcription: the shipped loop is inside `Iterator::for_each` → `Enumerate::fold` + /// → `I::fold` (core), where no loop contract can be attached, and `Enumerate::fold` keeps + /// its index in a closure that a loop contract lower down could neither name nor re-pin + /// after havocking. The transcription relies on `Iterator`'s documented equivalence between + /// `fold` and repeated `next()`. Its loop-contract proof is a partial-correctness proof + /// (Kani's loop contracts assume termination); termination follows from the exact + /// `size_hint` of the `TrustedLen` iterators every caller passes. `loop_decreases` is not + /// used because at the pinned Kani it conflicts with an explicit `loop_modifies`. + /// + /// Callers of `write_iter` whose iterator is reused after the call (the wrapping branch of + /// `write_iter_wrapping`, which passes `Take>`) are verified with this + /// helper replaced by `write_iter`'s contract plus the consumption of the iterator + /// (`verify::write_iter_contract_replacement`), because a loop contract cannot survive the + /// havocking of that reference-carrying adapter. #[cfg(kani)] #[inline] unsafe fn write_iter_loop( @@ -4027,15 +4072,155 @@ impl From<[T; N]> for VecDeque { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { + //! Kani proofs for Challenge 25. + //! + //! # Method + //! + //! Every harness starts from [`any_deque`]: a real allocation of symbolic capacity, a + //! symbolic `head` over every physical index and a symbolic `len` (so both the contiguous + //! and the wrapped ring layout are explored), with exactly the logical range initialized. + //! There is no `kani::unwind` and no length constant in any proof; the only bound on sizes + //! is CBMC's object model (`MAX_ALLOCATION_BYTES`). The 13 unsafe functions carry + //! `#[requires]`/`#[ensures]`/`kani::modifies` contracts checked by `proof_for_contract` + //! harnesses; the 30 safe functions have `#[kani::proof]` harnesses. Loops are discharged + //! with loop contracts (`retain_mut`, `write_iter_loop`). + //! + //! # Element shapes (generic `T`) + //! + //! Kani rejects a `#[kani::proof]` on a generic function, so each harness body is written + //! once for arbitrary `T` and instantiated over element *shapes* chosen to cover every + //! property of `T` that the code observes. `VecDeque` is parametric in `T` except through + //! `size_of`/`align_of` (allocation and pointer arithmetic), `T::IS_ZST` (the branches that + //! skip the buffer), moves of opaque values, and the drop glue `ptr::drop_in_place::<[T]>` + //! in `truncate`, `drain` and `Drop for VecDeque`; it never branches on `needs_drop` or on + //! element values (the only value-dependent code is the user closures, which the harnesses + //! make nondeterministic). + //! + //! | shape | size | align | `needs_drop` / non-`Copy` | validity invariant | + //! |---|---|---|---|---| + //! | `()` | 0 | 1 | no | no | + //! | `u8` | 1 | 1 | no | no | + //! | `bool` | 1 | 1 | no | yes (`0`/`1`) | + //! | `[u8; 3]` | 3 | 1 | no | no | + //! | `u64` | 8 | 8 | no | no | + //! | [`Al16`] | 16 | 16 | no | no | + //! | [`WithDrop`] | 1 | 1 | yes | no | + //! + //! `u8`, `u64` and `()` instantiate every harness (plus `[u8; 3]` on the cheap ones); + //! `bool`, `Al16` and `WithDrop` instantiate the harnesses whose targets exercise their + //! property (see the instantiation lists). For `WithDrop` the unbounded harnesses cover + //! every target that drops at most single elements; the slice drop glue + //! (`drop_in_place::<[T]>`, a compiler-generated loop that cannot carry a loop contract) is + //! checked bounded (`len <= 4`) in [`bounded_evidence`]. Generators write pre-existing + //! elements with one symbolic byte per region (a valid bit pattern of the shape, + //! [`Shape::any_fill`]); elements that enter through the API are per-element `kani::any()`. + //! Representative shapes are the closest Kani can come to the challenge's "no + //! monomorphization" clause. + //! + //! # Stubs and the `write_iter` transcription + //! + //! Everything a harness assumes about a callee is either its verified contract or one of + //! the items below, each with the harness that checks what it hides: + //! + //! | replacement | replaces | asserts | over-approximates | evidence | residual argument | + //! |---|---|---|---|---|---| + //! | `write_iter_loop` (cfg(kani) body of `write_iter`) | the shipped `for_each` statement | — | — (transcription) | `bounded_evidence::bounded_write_iter_shipped_text_*` runs the shipped statement (`write_iter_for_each`) against the same contract, `n <= 4` | `Iterator::fold` ≡ repeated `next()`; see `write_iter_loop`'s doc for why no loop contract can reach the shipped loop | + //! | [`VecDeque::write_iter_contract_replacement`] (and its `_drop` variant for `resize_with`) | `write_iter_loop` | `write_iter`'s precondition, via `write_iter_precondition` | `write_iter`'s `modifies` region gets an arbitrary fill; `written += hi`; iterator advanced by `hi` | `bounded_write_iter_wrapping_shipped_text_u8` (the branch with the shipped statement iterating) and `bounded_replacement_advance_by_matches_next_u8` (`advance_by(hi)` ≡ `hi` × `next()`) | exact-`hi` = `TrustedLen` exactness (asserted `lo == hi`) | + //! | [`stub_ptr_rotate`] (`check_make_contiguous_*` only) | `core::slice::rotate::ptr_rotate` | its documented precondition (range writable) | leaves memory untouched | `bounded_evidence::bounded_rotate_permutes_range_u8`: the real `rotate_left`/`rotate_right` on ranges of every length and amount up to eight, symbolic contents, guard bytes — exactly the rotated sequence, nothing else written | a rotation only permutes initialized slots; `make_contiguous` does nothing value-dependent afterwards | + //! + //! Loop-contract proofs are partial-correctness proofs at the pinned Kani (termination is + //! assumed); the loops involved terminate by the exact `size_hint` of `TrustedLen` + //! iterators (`write_iter_loop`) and by `cur` reaching `len` (`retain_mut`). + //! + //! # Kani limitations at the pinned version (`152c6a8`) + //! + //! 1. `stub_verified` on a contract whose `modifies` names a slice ICEs (kani#3682; the fix, + //! kani#4749, is 92 commits after the pin), and `kani::stub` of a contracted function is + //! rejected (kani#4591). Hence the contract-free `write_iter_loop` is the stub target. + //! Even with kani#4749, `stub_verified(write_iter)` would not prove the wrapping branch: + //! the generated replacement drops the by-value `Take>` unconsumed, + //! so the second call would see the whole iterator again (see + //! `write_iter_contract_replacement`). + //! 2. A loop contract cannot survive the havocking of a loop-carried adapter holding a + //! `&mut` (`Take>`): its private fields cannot be re-pinned. + //! 3. A stub must be a method when the original is one: signatures are compared by the + //! position of their own generic parameters. + //! 4. CBMC aborts on a `loop_modifies` target that is a zero-sized closure (kani#4786), so + //! `retain_mut`'s loop contracts do not list the predicate. + //! 5. `loop_decreases` cannot be combined with an explicit `loop_modifies`. + //! 6. `-Z uninit-checks` and `-Z valid-value-checks` are not enabled by CI (the former + //! rejects alloc at this pin, kani#3300); reading uninitialized memory and invalid values + //! are therefore only excluded by construction (initialized ranges, valid fills). + use core::iter::TrustedLen; use core::marker::PhantomData; use core::mem::SizedTypeProperties; + use core::sync::atomic::AtomicUsize; + use core::sync::atomic::Ordering::Relaxed; use core::{cmp, kani, ptr}; use crate::alloc::Layout; use crate::collections::VecDeque; use crate::vec::Vec; + // --------------------------------------------------------------------------------------- + // Element shapes + // --------------------------------------------------------------------------------------- + + /// An element type the generic harness bodies are instantiated with (see the shape matrix + /// in the module documentation). `any_fill` is the byte the generators write into every + /// byte of a pre-existing element; it must be a valid bit pattern for `Self`, which is why + /// types with a validity invariant override it. + pub(super) trait Shape: kani::Arbitrary { + fn any_fill() -> u8 { + kani::any() + } + } + + impl Shape for u8 {} + impl Shape for u64 {} + impl Shape for [u8; 3] {} + impl Shape for () {} + + /// Validity invariant: only the bit patterns `0` and `1` are valid. + impl Shape for bool { + fn any_fill() -> u8 { + kani::any_where(|b: &u8| *b <= 1) + } + } + + /// Alignment larger than any primitive's (`align_of == size_of == 16`). + #[derive(kani::Arbitrary)] + #[repr(align(16))] + pub(super) struct Al16(u8); + impl Shape for Al16 {} + + /// Number of `WithDrop` destructors that have run. Reset by the harnesses that assert on it + /// (`bounded_evidence`); the other harnesses only require that no destructor runs on an + /// uninitialized or already-moved slot, which Kani's memory checks enforce. + pub(super) static DROPS: AtomicUsize = AtomicUsize::new(0); + + /// `needs_drop` (and therefore non-`Copy`, move-only) element: its destructor counts itself + /// and reads its payload. + #[derive(kani::Arbitrary)] + pub(super) struct WithDrop(u8); + impl Drop for WithDrop { + fn drop(&mut self) { + DROPS.fetch_add(1, Relaxed); + core::hint::black_box(self.0); + } + } + impl Shape for WithDrop {} + + /// Ends a harness that owns `deque`. For shapes without a destructor the deque is dropped, + /// exercising `Drop for VecDeque` (whose `ptr::drop_in_place::<[T]>` is then a no-op). For + /// `needs_drop` shapes it is leaked: `drop_in_place::<[T]>` is a compiler-generated loop of + /// symbolic length that cannot carry a loop contract, so the drop-glue paths are checked + /// separately, bounded, in `bounded_evidence`. + pub(super) fn finish(deque: VecDeque) { + if core::mem::needs_drop::() { core::mem::forget(deque) } else { drop(deque) } + } + /// A non-vacuity witness for a path through the ring buffer. Zero-sized element types never /// touch the buffer (every such path is excluded by `T::IS_ZST` checks in the code), so the /// witness is only meaningful, and only required, for sized `T`. (A macro rather than a @@ -4065,11 +4250,13 @@ mod verify { /// * `head` ranges over every valid physical index and `len` over `0..=cap`, so both the /// contiguous (`head + len <= cap`) and the wrapped (`head + len > cap`) ring layouts are /// explored (see the `kani::cover` witnesses). - /// * Exactly the logical range `head..head + len` (wrapping at `cap`) is initialized, with an - /// arbitrary byte pattern; slots outside it stay uninitialized. The element types used by - /// the harnesses have no validity invariant, so any byte pattern is a valid `T`, and no - /// proof depends on the element values. - pub(super) fn any_deque() -> VecDeque { + /// * Exactly the logical range `head..head + len` (wrapping at `cap`) is initialized, every + /// byte with the shape's arbitrary valid fill byte (`Shape::any_fill`); slots outside it + /// stay uninitialized. `VecDeque` never branches on element values (the only + /// value-dependent code is the user closures, which the harnesses make nondeterministic, + /// and the elements `AnyIter` yields are per-element `kani::any()`), so one symbolic byte + /// per initialized region loses nothing. + pub(super) fn any_deque() -> VecDeque { let requested: usize = kani::any(); kani::assume(Layout::array::(requested).is_ok()); kani::assume( @@ -4082,7 +4269,7 @@ mod verify { let head: usize = if cap == 0 { 0 } else { kani::any_where(|h: &usize| *h < cap) }; let len: usize = kani::any_where(|l: &usize| *l <= cap); if !T::IS_ZST && len > 0 { - let fill: u8 = kani::any(); + let fill: u8 = T::any_fill(); let head_room = cap - head; unsafe { if len <= head_room { @@ -4107,7 +4294,7 @@ mod verify { pub(super) fn touch(deque: &VecDeque) { let i: usize = kani::any(); if let Some(elem) = deque.get(i) { - let _ = unsafe { ptr::read(elem) }; + core::mem::forget(unsafe { ptr::read(elem) }); } assert!(deque.invariant_holds()); } @@ -4159,70 +4346,94 @@ mod verify { /// Contract replacement for the loop of `VecDeque::write_iter` (`write_iter_loop`), used /// when verifying the callers of `write_iter` (`write_iter_wrapping`, `resize_with`). /// `write_iter` itself, loop included, is verified against its real body by - /// `check_write_iter_*`. - /// - /// This is what `#[kani::stub_verified(write_iter)]` would generate. It is written by hand - /// because the pinned Kani (a) cannot generate the replacement of a contract whose - /// `modifies` clause names a slice (kani-compiler `transform/contracts.rs` resolves - /// `write_any_slice` with the slice type itself as the element type and ICEs in - /// `reachability.rs`), and (b) cannot `kani::stub` a function that carries a contract - /// (model-checking/kani#4591); hence the contract-free helper is the stub target. - /// - /// It *asserts* the precondition of `write_iter`'s contract (so a caller violating it fails - /// its proof), then models every behaviour the contract permits: the iterator yields some - /// `n <= hi` elements, exactly the slots `dst..dst + n` receive arbitrary values, and - /// `*written` grows by `n`. The iterator is dropped rather than driven, so no loop is needed. - unsafe fn stub_write_iter_loop( - deque: &mut VecDeque, - dst: usize, - mut iter: impl Iterator, - written: &mut usize, - ) { - let n = unsafe { model_write_iter(deque, dst, &iter, written) }; - // Consume the elements from the iterator exactly as the real loop does, so that an - // iterator shared with a later call (`write_iter_wrapping`'s wrapping branch borrows - // `iter` for the first call and passes it on to the second) reports the right - // remaining length. `advance_by` is O(1) for the harness iterator and the `Take` / - // `ByRefSized` adapters the callee wraps it in. - assert!(iter.advance_by(n).is_ok()); - } - - /// Like [`stub_write_iter_loop`] but drops the iterator instead of advancing it. Only valid - /// where the iterator is not observed after the call, i.e. in the non-wrapping branch of - /// `write_iter_wrapping` (used by the `resize_with` harnesses, whose `Take>` - /// iterator cannot be advanced without a loop). - unsafe fn stub_write_iter_loop_drop( - deque: &mut VecDeque, - dst: usize, - iter: impl Iterator, - written: &mut usize, - ) { - let _ = unsafe { model_write_iter(deque, dst, &iter, written) }; - drop(iter); - } + /// `check_write_iter_*`. (Running the real loop inside the callers was tried at the pinned + /// Kani: the loop contract is then instrumented for the `Take>` + /// instance of the wrapping branch as well, and neither `check_resize_with_u8` nor a + /// direct-branch-only `write_iter_wrapping` harness finished within 20 minutes.) + /// + /// This is what `#[kani::stub_verified(write_iter)]` would generate, **plus one step**. It + /// is written by hand because the pinned Kani (a) ICEs when generating the replacement of a + /// contract whose `modifies` clause names a slice (model-checking/kani#3682; the fix, + /// model-checking/kani#4749, postdates the pin) and (b) cannot `kani::stub` a function that + /// carries a contract (model-checking/kani#4591); hence the contract-free helper is the + /// stub target. The extra step is `iter.advance_by(hi)`: a pure contract replacement drops + /// the by-value `Take>` unconsumed, so the caller's second `write_iter` + /// call would see the whole iterator again and could write past `len` — the caller's own + /// `ensures`/`modifies` are only provable with the consumption modelled. This step is what + /// the loop does (it calls `next()` until `None`, i.e. exactly `hi` times for an exact + /// hint), and `bounded_evidence::bounded_write_iter_wrapping_shipped_text_u8` runs the + /// shipped statement on this very adapter stack, bounded, and + /// `bounded_evidence::bounded_replacement_advance_by_matches_next_u8` checks + /// `advance_by(hi)` against `hi` calls of `next()` on it. + /// + /// What it does: *asserts* the precondition of `write_iter`'s contract — through the same + /// predicate the contract uses, `write_iter_precondition`, so the two cannot drift — then + /// models the effect the contract permits: exactly the slots `dst..dst + hi` receive an + /// arbitrary valid fill (the `modifies` region, `slots(dst, hi)`; one symbolic byte per + /// region, since no proof reads element values), `*written` grows by `hi`, and the iterator + /// is advanced by `hi`. Writing exactly `hi` rather than the contract's `<= hi` is the one + /// assumption beyond the contract; it is the `TrustedLen` exactness every caller relies on + /// (asserted here as `lo == hi`) and what the loop does with such an iterator. + /// + /// It is a method rather than a free function because the pinned Kani compares a stub's + /// signature with the original's by the position of their *own* generic parameters (the + /// `impl Iterator` argument here); a free function would put `T` and `A` in those + /// positions and be rejected ("Cannot stub … Expected type `&mut VecDeque` …"). + impl VecDeque { + pub(super) unsafe fn write_iter_contract_replacement( + &mut self, + dst: usize, + mut iter: impl Iterator, + written: &mut usize, + ) { + let (lo, hi) = iter.size_hint(); + kani::assert( + self.write_iter_precondition(dst, hi, *written), + "write_iter precondition", + ); + let hi = hi.unwrap(); + kani::assert(lo == hi, "write_iter callers pass TrustedLen iterators"); + if !T::IS_ZST && hi > 0 { + unsafe { ptr::write_bytes(self.ptr().add(dst), T::any_fill(), hi) }; + } + *written += hi; + // Consume the elements exactly as the real loop does, so that an iterator shared + // with a later call (`write_iter_wrapping`'s wrapping branch borrows `iter` for the + // first call and passes it on to the second) reports the right remaining length. + // `advance_by` is O(1) for the harness iterator and the `Take` / `ByRefSized` + // adapters the callee wraps it in. + kani::assert( + iter.advance_by(hi).is_ok(), + "write_iter replacement: iterator advanced by hi", + ); + } - /// Shared model of one `write_iter` call: checks the contract's precondition, requires the - /// exact size hint every `TrustedLen` caller guarantees, havocs exactly the slots that - /// receive elements and advances `*written`. Returns the number of elements written. - unsafe fn model_write_iter( - deque: &mut VecDeque, - dst: usize, - iter: &impl Iterator, - written: &mut usize, - ) -> usize { - let (lo, hi) = iter.size_hint(); - let hi = hi.expect("write_iter: iterator must have an upper size bound"); - assert!(lo == hi, "write_iter callers pass TrustedLen iterators"); - assert!(dst.checked_add(hi).is_some_and(|end| end <= deque.capacity())); - assert!(written.checked_add(hi).is_some()); - if !T::IS_ZST && hi > 0 { - unsafe { ptr::write_bytes(deque.ptr().add(dst), kani::any::(), hi) }; + /// Like [`Self::write_iter_contract_replacement`] but drops the iterator instead of + /// advancing it. Only valid where the iterator is not observed after the call, i.e. in + /// the non-wrapping branch of `write_iter_wrapping`; used by the `resize_with` + /// harnesses, whose `Take>` iterator cannot be advanced without a loop. + pub(super) unsafe fn write_iter_contract_replacement_drop( + &mut self, + dst: usize, + iter: impl Iterator, + written: &mut usize, + ) { + let (lo, hi) = iter.size_hint(); + kani::assert( + self.write_iter_precondition(dst, hi, *written), + "write_iter precondition", + ); + let hi = hi.unwrap(); + kani::assert(lo == hi, "write_iter callers pass TrustedLen iterators"); + if !T::IS_ZST && hi > 0 { + unsafe { ptr::write_bytes(self.ptr().add(dst), T::any_fill(), hi) }; + } + *written += hi; + drop(iter); } - *written += hi; - hi } - fn check_write_iter() { + fn check_write_iter() { let mut deque = any_deque::(); let dst: usize = kani::any(); let n: usize = kani::any(); @@ -4232,9 +4443,10 @@ mod verify { assert_eq!(written, before + n); kani::cover(n > 1, "write_iter: more than one element written"); kani::cover(dst > 0 && n > 0, "write_iter: non-zero destination"); + finish(deque); } - fn check_write_iter_wrapping() { + fn check_write_iter_wrapping() { let mut deque = any_deque::(); let dst: usize = kani::any(); let len: usize = kani::any(); @@ -4246,9 +4458,10 @@ mod verify { kani::cover(len > deque.capacity() - dst, "write_iter_wrapping: wrapping branch"); kani::cover(n > 0 && len <= deque.capacity() - dst, "write_iter_wrapping: direct branch"); touch(&deque); + finish(deque); } - fn check_copy() { + fn check_copy() { let mut deque = any_deque::(); let src: usize = kani::any(); let dst: usize = kani::any(); @@ -4259,7 +4472,7 @@ mod verify { touch(&deque); } - fn check_copy_nonoverlapping() { + fn check_copy_nonoverlapping() { let mut deque = any_deque::(); let src: usize = kani::any(); let dst: usize = kani::any(); @@ -4269,7 +4482,7 @@ mod verify { touch(&deque); } - fn check_wrap_copy() { + fn check_wrap_copy() { let mut deque = any_deque::(); let src: usize = kani::any(); let dst: usize = kani::any(); @@ -4314,29 +4527,32 @@ mod verify { touch(&deque); } - fn check_buffer_read() { + fn check_buffer_read() { let mut deque = any_deque::(); let off: usize = kani::any(); let value = unsafe { deque.buffer_read(off) }; core::mem::forget(value); kani::cover(off > 0, "buffer_read: non-zero offset"); + finish(deque); } - fn check_buffer_write() { + fn check_buffer_write() { let mut deque = any_deque::(); let off: usize = kani::any(); let slot = unsafe { deque.buffer_write(off, kani::any()) }; - let _ = unsafe { ptr::read(slot) }; + core::mem::forget(unsafe { ptr::read(slot) }); kani::cover(off > 0, "buffer_write: non-zero offset"); + finish(deque); } - fn check_push_unchecked() { + fn check_push_unchecked() { let mut deque = any_deque::(); let old_len = deque.len; unsafe { deque.push_unchecked(kani::any()) }; assert_eq!(deque.len, old_len + 1); kani::cover(old_len >= deque.capacity() - deque.head, "push_unchecked: wrapped write"); touch(&deque); + finish(deque); } // --------------------------------------------------------------------------------------- @@ -4355,7 +4571,7 @@ mod verify { assert!(core::ub_checks::can_write(ptr::slice_from_raw_parts_mut(start, len))); } - fn check_make_contiguous() { + fn check_make_contiguous() { let mut deque = any_deque::(); let len = deque.len; let cap = deque.capacity(); @@ -4365,7 +4581,7 @@ mod verify { let slice = deque.make_contiguous(); assert_eq!(slice.len(), len); if len > 0 { - let _ = unsafe { ptr::read(&slice[len - 1]) }; + core::mem::forget(unsafe { ptr::read(&slice[len - 1]) }); } assert!(deque.is_contiguous()); let head_len = cap - head; @@ -4412,11 +4628,16 @@ mod verify { /// Lays out a logical ring of `len` elements starting at `head` inside the first `ring_cap` /// slots of `deque`'s buffer (`ring_cap <= deque.capacity()`, `head < ring_cap` unless /// `ring_cap == 0`, `len <= ring_cap`): initializes exactly those slots and sets the fields. - pub(super) fn init_ring(deque: &mut VecDeque, ring_cap: usize, head: usize, len: usize) { + pub(super) fn init_ring( + deque: &mut VecDeque, + ring_cap: usize, + head: usize, + len: usize, + ) { assert!(ring_cap <= deque.capacity() && len <= ring_cap); assert!(head < ring_cap || (ring_cap == 0 && head == 0)); if !T::IS_ZST && len > 0 { - let fill: u8 = kani::any(); + let fill: u8 = T::any_fill(); let head_room = ring_cap - head; unsafe { if len <= head_room { @@ -4432,7 +4653,7 @@ mod verify { } /// A `Vec` of symbolic length whose elements are all initialized. - pub(super) fn any_vec() -> Vec { + pub(super) fn any_vec() -> Vec { let len: usize = kani::any(); kani::assume(Layout::array::(len).is_ok()); kani::assume( @@ -4440,13 +4661,13 @@ mod verify { ); let mut vec = Vec::::with_capacity(len); if !T::IS_ZST && len > 0 { - unsafe { ptr::write_bytes(vec.as_mut_ptr(), kani::any::(), len) }; + unsafe { ptr::write_bytes(vec.as_mut_ptr(), T::any_fill(), len) }; } unsafe { vec.set_len(len) }; vec } - fn check_buffer_range() { + fn check_buffer_range() { let deque = any_deque::(); let start: usize = kani::any(); let end: usize = kani::any(); @@ -4459,7 +4680,7 @@ mod verify { core::mem::forget(deque); } - fn check_copy_slice() { + fn check_copy_slice() { let mut deque = any_deque::(); let src = any_vec::(); let dst: usize = kani::any(); @@ -4469,7 +4690,7 @@ mod verify { touch(&deque); } - fn check_handle_capacity_increase() { + fn check_handle_capacity_increase() { let mut deque = any_empty_deque::(); let new_cap = deque.capacity(); let old_cap: usize = kani::any_where(|c: &usize| *c <= new_cap); @@ -4489,13 +4710,13 @@ mod verify { touch(&deque); } - fn check_from_contiguous_raw_parts_in() { + fn check_from_contiguous_raw_parts_in() { let vec = any_empty_deque_vec::(); let (ptr, _, capacity, alloc) = vec.into_raw_parts_with_alloc(); let start: usize = kani::any(); let end: usize = kani::any(); if !T::IS_ZST && start <= end && end <= capacity && end > start { - unsafe { ptr::write_bytes(ptr.add(start), kani::any::(), end - start) }; + unsafe { ptr::write_bytes(ptr.add(start), T::any_fill(), end - start) }; } let deque = unsafe { VecDeque::from_contiguous_raw_parts_in(ptr, start..end, capacity, alloc) }; @@ -4511,6 +4732,7 @@ mod verify { start == 0 && end == 0 && capacity > 0, "from_contiguous_raw_parts_in: empty range", ); + finish(deque); } /// A `Vec` with symbolic capacity and no elements, used to obtain raw parts. @@ -4525,7 +4747,7 @@ mod verify { Vec::::with_capacity(requested) } - fn check_abort_shrink() { + fn check_abort_shrink() { let mut deque = any_empty_deque::(); let cap = deque.capacity(); let target_cap: usize = kani::any_where(|c: &usize| *c <= cap); @@ -4550,7 +4772,7 @@ mod verify { touch(&deque); } - fn check_rotate_left_inner() { + fn check_rotate_left_inner() { let mut deque = any_deque::(); let mid: usize = kani::any(); unsafe { deque.rotate_left_inner(mid) }; @@ -4558,7 +4780,7 @@ mod verify { touch(&deque); } - fn check_rotate_right_inner() { + fn check_rotate_right_inner() { let mut deque = any_deque::(); let k: usize = kani::any(); unsafe { deque.rotate_right_inner(k) }; @@ -4582,19 +4804,20 @@ mod verify { })); } - fn check_get() { + fn check_get() { let deque = any_deque::(); let i: usize = kani::any(); let elem = deque.get(i); assert_eq!(elem.is_some(), i < deque.len()); if let Some(elem) = elem { - let _ = unsafe { ptr::read(elem) }; + core::mem::forget(unsafe { ptr::read(elem) }); } kani::cover(i > 0 && i < deque.len(), "get: in-bounds non-front index"); kani::cover(i >= deque.len(), "get: out-of-bounds index"); + finish(deque); } - fn check_get_mut() { + fn check_get_mut() { let mut deque = any_deque::(); let i: usize = kani::any(); let len = deque.len(); @@ -4605,9 +4828,10 @@ mod verify { } kani::cover(i > 0 && i < len, "get_mut: in-bounds non-front index"); touch(&deque); + finish(deque); } - fn check_swap() { + fn check_swap() { let mut deque = any_deque::(); let len = deque.len(); let i: usize = kani::any_where(|x: &usize| *x < len); @@ -4615,22 +4839,23 @@ mod verify { deque.swap(i, j); kani::cover(i != j, "swap: distinct indices"); touch(&deque); + finish(deque); } - fn check_as_slices() { + fn check_as_slices() { let deque = any_deque::(); let (a, b) = deque.as_slices(); assert_eq!(a.len() + b.len(), deque.len()); if let Some(last) = a.last() { - let _ = unsafe { ptr::read(last) }; + core::mem::forget(unsafe { ptr::read(last) }); } if let Some(last) = b.last() { - let _ = unsafe { ptr::read(last) }; + core::mem::forget(unsafe { ptr::read(last) }); } kani::cover(!a.is_empty() && !b.is_empty(), "as_slices: both halves non-empty"); } - fn check_as_mut_slices() { + fn check_as_mut_slices() { let mut deque = any_deque::(); let len = deque.len(); let (a, b) = deque.as_mut_slices(); @@ -4651,21 +4876,21 @@ mod verify { (start, end) } - fn check_range() { + fn check_range() { let deque = any_deque::(); let (start, end) = any_subrange(deque.len()); let mut iter = deque.range(start..end); assert_eq!(iter.len(), end - start); if let Some(first) = iter.next() { - let _ = unsafe { ptr::read(first) }; + core::mem::forget(unsafe { ptr::read(first) }); } if let Some(last) = iter.next_back() { - let _ = unsafe { ptr::read(last) }; + core::mem::forget(unsafe { ptr::read(last) }); } kani::cover(end - start > 2, "range: more than two elements"); } - fn check_range_mut() { + fn check_range_mut() { let mut deque = any_deque::(); let (start, end) = any_subrange(deque.len()); let mut iter = deque.range_mut(start..end); @@ -4680,7 +4905,7 @@ mod verify { touch(&deque); } - fn check_drain() { + fn check_drain() { let mut deque = any_deque::(); let len = deque.len(); let (start, end) = any_subrange(len); @@ -4709,7 +4934,7 @@ mod verify { touch(&deque); } - fn check_pop_front() { + fn check_pop_front() { let mut deque = any_deque::(); let len = deque.len(); let elem = deque.pop_front(); @@ -4718,9 +4943,10 @@ mod verify { core::mem::forget(elem); kani::cover(len > 1, "pop_front: elements remain"); touch(&deque); + finish(deque); } - fn check_pop_back() { + fn check_pop_back() { let mut deque = any_deque::(); let len = deque.len(); let elem = deque.pop_back(); @@ -4729,9 +4955,10 @@ mod verify { core::mem::forget(elem); kani::cover(len > 1, "pop_back: elements remain"); touch(&deque); + finish(deque); } - fn check_push_front() { + fn check_push_front() { let mut deque = any_deque::(); let len = deque.len(); let full = deque.is_full(); @@ -4741,9 +4968,10 @@ mod verify { cover_buffer_path!(T, full && len > 0, "push_front: buffer grown"); kani::cover(!full && len > 0, "push_front: no growth"); touch(&deque); + finish(deque); } - fn check_push_back() { + fn check_push_back() { let mut deque = any_deque::(); let len = deque.len(); let full = deque.is_full(); @@ -4753,9 +4981,10 @@ mod verify { cover_buffer_path!(T, full && len > 0, "push_back: buffer grown"); kani::cover(!full && len > 0, "push_back: no growth"); touch(&deque); + finish(deque); } - fn check_reserve() { + fn check_reserve() { let mut deque = any_deque::(); let len = deque.len(); let old_cap = deque.capacity(); @@ -4769,7 +4998,7 @@ mod verify { touch(&deque); } - fn check_reserve_exact() { + fn check_reserve_exact() { let mut deque = any_deque::(); let len = deque.len(); let old_cap = deque.capacity(); @@ -4783,7 +5012,7 @@ mod verify { touch(&deque); } - fn check_try_reserve() { + fn check_try_reserve() { let mut deque = any_deque::(); let len = deque.len(); let old_cap = deque.capacity(); @@ -4802,7 +5031,7 @@ mod verify { touch(&deque); } - fn check_try_reserve_exact() { + fn check_try_reserve_exact() { let mut deque = any_deque::(); let len = deque.len(); let old_cap = deque.capacity(); @@ -4821,7 +5050,7 @@ mod verify { touch(&deque); } - fn check_shrink_to() { + fn check_shrink_to() { let mut deque = any_deque::(); let len = deque.len(); let head = deque.head; @@ -4857,7 +5086,7 @@ mod verify { touch(&deque); } - fn check_truncate() { + fn check_truncate() { let mut deque = any_deque::(); let len = deque.len(); let front_len = deque.as_slices().0.len(); @@ -4873,7 +5102,7 @@ mod verify { touch(&deque); } - fn check_insert() { + fn check_insert() { let mut deque = any_deque::(); let len = deque.len(); let full = deque.is_full(); @@ -4887,7 +5116,7 @@ mod verify { touch(&deque); } - fn check_remove() { + fn check_remove() { let mut deque = any_deque::(); let len = deque.len(); let index: usize = kani::any(); @@ -4901,9 +5130,10 @@ mod verify { "remove: front half shifted", ); touch(&deque); + finish(deque); } - fn check_split_off() { + fn check_split_off() { let mut deque = any_deque::(); let len = deque.len(); let first_len = deque.as_slices().0.len(); @@ -4918,9 +5148,11 @@ mod verify { ); touch(&deque); touch(&other); + finish(deque); + finish(other); } - fn check_append() { + fn check_append() { let mut deque = any_deque::(); let mut other = any_deque::(); let len = deque.len(); @@ -4934,9 +5166,11 @@ mod verify { kani::cover(len + other_len <= old_cap && other_len > 0 && len > 0, "append: in place"); touch(&deque); touch(&other); + finish(deque); + finish(other); } - fn check_retain_mut() { + fn check_retain_mut() { let mut deque = any_deque::(); let len = deque.len(); deque.retain_mut(|elem| { @@ -4951,7 +5185,7 @@ mod verify { touch(&deque); } - fn check_grow() { + fn check_grow() { let mut deque = any_deque::(); kani::assume(deque.is_full()); let len = deque.len(); @@ -4967,13 +5201,14 @@ mod verify { /// `Take>` iterator. That iterator cannot be advanced without a loop, so the /// contract replacement of `write_iter`'s loop can only model calls after which the /// iterator is not reused, i.e. the non-wrapping branch of `write_iter_wrapping` (see - /// `stub_write_iter_loop_drop`). The two `resize_with` harnesses therefore restrict the - /// appended elements to not wrap around the end of the buffer, in two complementary ways; - /// the wrapping write path itself is verified by `check_write_iter_wrapping_*`. + /// `write_iter_contract_replacement_drop`). The two `resize_with` harnesses therefore + /// restrict the appended elements to not wrap around the end of the buffer, in two + /// complementary ways; the wrapping write path itself is verified by + /// `check_write_iter_wrapping_*`. /// /// Variant 1: arbitrary (possibly wrapped) deque, capacity reserved up front so that the /// appended elements fit behind the last element without wrapping. - fn check_resize_with() { + fn check_resize_with() { let mut deque = any_deque::(); let len = deque.len(); let new_len: usize = kani::any(); @@ -4996,7 +5231,7 @@ mod verify { /// Variant 2: contiguous deque starting at `head == 0`, so that the growth performed by /// `resize_with` itself (`reserve` → `handle_capacity_increase`, case A) keeps the appended /// elements from wrapping. - fn check_resize_with_grow() { + fn check_resize_with_grow() { let mut deque = any_deque::(); kani::assume(deque.head == 0); let len = deque.len(); @@ -5015,7 +5250,7 @@ mod verify { touch(&deque); } - fn check_rotate_left() { + fn check_rotate_left() { let mut deque = any_deque::(); let len = deque.len(); let n: usize = kani::any_where(|n: &usize| *n <= len); @@ -5026,7 +5261,7 @@ mod verify { touch(&deque); } - fn check_rotate_right() { + fn check_rotate_right() { let mut deque = any_deque::(); let len = deque.len(); let n: usize = kani::any_where(|n: &usize| *n <= len); @@ -5088,19 +5323,19 @@ mod verify { contract_harnesses!( write_iter_wrapping, check_write_iter_wrapping, - [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop)], + [kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_contract_replacement)], [u8 => check_write_iter_wrapping_u8] ); contract_harnesses!( write_iter_wrapping, check_write_iter_wrapping, - [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop)], + [kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_contract_replacement)], [u64 => check_write_iter_wrapping_u64] ); contract_harnesses!( write_iter_wrapping, check_write_iter_wrapping, - [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop)], + [kani::stub(VecDeque::<()>::write_iter_loop, VecDeque::<()>::write_iter_contract_replacement)], [() => check_write_iter_wrapping_unit] ); contract_harnesses!(handle_capacity_increase, check_handle_capacity_increase, [u8 => check_handle_capacity_increase_u8, u64 => check_handle_capacity_increase_u64, () => check_handle_capacity_increase_unit]); @@ -5138,22 +5373,22 @@ mod verify { proof_harnesses!(check_grow, [], [u8 => check_grow_u8]); proof_harnesses!( check_resize_with, - [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop_drop)], + [kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_contract_replacement_drop)], [u8 => check_resize_with_u8] ); proof_harnesses!( check_resize_with, - [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop_drop)], + [kani::stub(VecDeque::<()>::write_iter_loop, VecDeque::<()>::write_iter_contract_replacement_drop)], [() => check_resize_with_unit] ); proof_harnesses!( check_resize_with_grow, - [kani::stub(VecDeque::::write_iter_loop, stub_write_iter_loop_drop)], + [kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_contract_replacement_drop)], [u8 => check_resize_with_grow_u8] ); proof_harnesses!( check_resize_with_grow, - [kani::stub(VecDeque::<()>::write_iter_loop, stub_write_iter_loop_drop)], + [kani::stub(VecDeque::<()>::write_iter_loop, VecDeque::<()>::write_iter_contract_replacement_drop)], [() => check_resize_with_grow_unit] ); proof_harnesses!( @@ -5164,6 +5399,305 @@ mod verify { proof_harnesses!(check_rotate_left, [], [u8 => check_rotate_left_u8, () => check_rotate_left_unit]); proof_harnesses!(check_rotate_right, [], [u8 => check_rotate_right_u8, () => check_rotate_right_unit]); + // Additional shapes (see the shape matrix in the module documentation). `WithDrop` goes on + // the targets that move or read elements and drop at most one at a time; `Al16` and `bool` + // on the cheap allocation/read paths. The drop-glue paths are in `bounded_evidence`. + contract_harnesses!(push_unchecked, check_push_unchecked, [WithDrop => check_push_unchecked_withdrop, Al16 => check_push_unchecked_al16, bool => check_push_unchecked_bool]); + contract_harnesses!(buffer_read, check_buffer_read, [WithDrop => check_buffer_read_withdrop, Al16 => check_buffer_read_al16, bool => check_buffer_read_bool]); + contract_harnesses!(buffer_write, check_buffer_write, [WithDrop => check_buffer_write_withdrop, Al16 => check_buffer_write_al16]); + contract_harnesses!(buffer_range, check_buffer_range, [Al16 => check_buffer_range_al16]); + contract_harnesses!(copy, check_copy, [Al16 => check_copy_al16]); + contract_harnesses!(copy_nonoverlapping, check_copy_nonoverlapping, [Al16 => check_copy_nonoverlapping_al16]); + contract_harnesses!(write_iter, check_write_iter, [WithDrop => check_write_iter_withdrop, Al16 => check_write_iter_al16, bool => check_write_iter_bool]); + contract_harnesses!( + write_iter_wrapping, + check_write_iter_wrapping, + [kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_contract_replacement)], + [WithDrop => check_write_iter_wrapping_withdrop] + ); + contract_harnesses!(from_contiguous_raw_parts_in, check_from_contiguous_raw_parts_in, [WithDrop => check_from_contiguous_raw_parts_in_withdrop, Al16 => check_from_contiguous_raw_parts_in_al16]); + proof_harnesses!(check_get, [], [WithDrop => check_get_withdrop, Al16 => check_get_al16, bool => check_get_bool]); + proof_harnesses!(check_get_mut, [], [WithDrop => check_get_mut_withdrop]); + proof_harnesses!(check_swap, [], [WithDrop => check_swap_withdrop]); + proof_harnesses!(check_pop_front, [], [WithDrop => check_pop_front_withdrop, Al16 => check_pop_front_al16, bool => check_pop_front_bool]); + proof_harnesses!(check_pop_back, [], [WithDrop => check_pop_back_withdrop]); + proof_harnesses!(check_push_front, [], [WithDrop => check_push_front_withdrop]); + proof_harnesses!(check_push_back, [], [WithDrop => check_push_back_withdrop, Al16 => check_push_back_al16, bool => check_push_back_bool]); + proof_harnesses!(check_remove, [], [WithDrop => check_remove_withdrop]); + proof_harnesses!(check_split_off, [], [WithDrop => check_split_off_withdrop, Al16 => check_split_off_al16]); + proof_harnesses!(check_append, [], [WithDrop => check_append_withdrop]); + proof_harnesses!(check_shrink_to, [], [Al16 => check_shrink_to_al16]); + + /// Bounded supplementary evidence. + /// + /// None of the harnesses in this module is the proof of any function listed in Challenge + /// 25. Each is supplementary evidence for one stub, one transcription or one drop-glue path + /// named in its doc comment, and this module is the only place in `verify` that uses + /// `#[kani::unwind]`. Every listed function keeps its unbounded harness in the parent + /// module. No harness here reaches a loop that carries a loop contract except the + /// `retain_mut` drop-glue one (Kani replaces such loops by their contracts regardless of the + /// unwind bound, which is fine there: only the drop glue is bounded); the `write_iter` + /// iteration is exercised through the contract-free `write_iter_for_each`, the shipped + /// statement. + mod bounded_evidence { + use core::iter::ByRefSized; + + use super::*; + + /// Bound on the iterator length / element count of every harness in this module. + const N: usize = 4; + + // ----------------------------------------------------------------------------------- + // Item 2: the shipped `for_each` statement of `write_iter` + // ----------------------------------------------------------------------------------- + + /// `write_iter`'s contract checked against the shipped `for_each` statement + /// (`write_iter_for_each`, substituted for `write_iter_loop`), the deque fully + /// symbolic, the iterator length bounded by `N`. + fn write_iter_shipped_text() { + let mut deque = any_deque::(); + let dst: usize = kani::any(); + let n: usize = kani::any(); + kani::assume(n <= N); + let mut written: usize = kani::any(); + let before = written; + unsafe { deque.write_iter(dst, AnyIter::::new(n), &mut written) }; + assert_eq!(written, before + n); + kani::cover(n == N && dst > 0, "shipped text: N elements written at a non-zero offset"); + finish(deque); + } + + macro_rules! shipped_text_harness { + ($ty:ty, $name:ident) => { + #[kani::proof_for_contract(VecDeque::<$ty>::write_iter)] + #[kani::stub(VecDeque::<$ty>::write_iter_loop, VecDeque::<$ty>::write_iter_for_each)] + #[kani::unwind(6)] + fn $name() { + write_iter_shipped_text::<$ty>(); + } + }; + } + shipped_text_harness!(u8, bounded_write_iter_shipped_text_u8); + shipped_text_harness!(u64, bounded_write_iter_shipped_text_u64); + shipped_text_harness!([u8; 3], bounded_write_iter_shipped_text_u8x3); + shipped_text_harness!((), bounded_write_iter_shipped_text_unit); + shipped_text_harness!(WithDrop, bounded_write_iter_shipped_text_withdrop); + + // ----------------------------------------------------------------------------------- + // Item 3: what `write_iter_contract_replacement` adds to `write_iter`'s contract + // ----------------------------------------------------------------------------------- + + /// The wrapping branch of `write_iter_wrapping` with the shipped statement doing the + /// iteration on the real adapter stack (`Take>`, then the + /// borrowed iterator itself): every element is written exactly once (`written == n`), + /// which is the consumption `write_iter_contract_replacement` models with + /// `advance_by(hi)`. + #[kani::proof_for_contract(VecDeque::::write_iter_wrapping)] + #[kani::stub(VecDeque::::write_iter_loop, VecDeque::::write_iter_for_each)] + #[kani::unwind(6)] + fn bounded_write_iter_wrapping_shipped_text_u8() { + let mut deque = any_deque::(); + let dst: usize = kani::any(); + let len: usize = kani::any(); + let n: usize = kani::any(); + kani::assume(n <= N); + let old_len = deque.len; + let written = unsafe { deque.write_iter_wrapping(dst, AnyIter::::new(n), len) }; + assert_eq!(written, n); + assert_eq!(deque.len, old_len + n); + kani::cover( + n > 1 && n > deque.capacity() - dst, + "shipped text, wrapping branch: both write_iter calls write", + ); + touch(&deque); + } + + /// `advance_by(hi)` — the step `write_iter_contract_replacement` adds to the contract — + /// leaves the borrowed iterator in the same state as `hi` calls of `next()` (what the + /// loop does), on the adapter stack `write_iter_wrapping` builds and on the bare + /// iterator, for `hi = size_hint().1` (the value the replacement uses; `Take::next` and + /// `Take::advance_by` differ only past the hint). + #[kani::proof] + #[kani::unwind(6)] + fn bounded_replacement_advance_by_matches_next_u8() { + let n: usize = kani::any(); + let k: usize = kani::any(); + kani::assume(n <= N && k <= N); + // The adapter stack of the wrapping branch's first call. + let mut a = AnyIter::::new(n); + let mut b = AnyIter::::new(n); + let mut ta = ByRefSized(&mut a).take(k); + let hi = ta.size_hint().1.unwrap(); + assert_eq!(ta.size_hint().0, hi); + assert!(ta.advance_by(hi).is_ok()); + let mut tb = ByRefSized(&mut b).take(k); + let mut steps = 0; + while let Some(_) = tb.next() { + steps += 1; + } + assert_eq!(steps, hi); + drop(ta); + drop(tb); + assert_eq!(a.size_hint(), b.size_hint()); + assert_eq!(a.size_hint().1, Some(n - hi)); + // The bare iterator (direct branch, and the wrapping branch's second call). + let mut c = AnyIter::::new(n); + let mut d = AnyIter::::new(n); + let hi = c.size_hint().1.unwrap(); + assert!(c.advance_by(hi).is_ok()); + let mut steps = 0; + while let Some(_) = d.next() { + steps += 1; + } + assert_eq!(steps, hi); + assert_eq!(c.size_hint(), d.size_hint()); + kani::cover(k > 0 && k < n, "Take budget smaller than the iterator"); + kani::cover(k > n, "Take budget larger than the iterator"); + } + + // ----------------------------------------------------------------------------------- + // Item 3: `stub_ptr_rotate` + // ----------------------------------------------------------------------------------- + + /// `<[u8]>::rotate_left` / `rotate_right` — the calls `make_contiguous` makes, hence + /// `core::slice::rotate::ptr_rotate` — on ranges of every length up to eight and every + /// rotation amount, with symbolic contents and a symbolic guard byte on each side: the + /// range holds exactly the rotated sequence afterwards and the guards are untouched, + /// i.e. `ptr_rotate` permutes the slots of the range and writes nothing else — what + /// `stub_ptr_rotate` abstracts for `check_make_contiguous_*`. Lengths and amounts are + /// enumerated rather than symbolic so that `ptr_rotate`'s algorithm selection is + /// concrete: only the selected, loop-free `ptr_rotate_memmove` is explored (the two + /// looping algorithms need `min(left, right) > 256` for `u8`, and would otherwise be + /// unwound although unreachable). + #[kani::proof] + #[kani::unwind(10)] + fn bounded_rotate_permutes_range_u8() { + const N: usize = 8; + for len in 0..=N { + for mid in 0..=len { + let mut buf: [u8; N + 2] = kani::any(); + let before = buf; + buf[1..1 + len].rotate_left(mid); + for i in 0..len { + assert_eq!(buf[1 + i], before[1 + (i + mid) % len]); + } + assert_eq!(buf[0], before[0]); + for i in 1 + len..N + 2 { + assert_eq!(buf[i], before[i]); + } + let mut buf: [u8; N + 2] = kani::any(); + let before = buf; + buf[1..1 + len].rotate_right(mid); + for i in 0..len { + assert_eq!(buf[1 + (i + mid) % len], before[1 + i]); + } + assert_eq!(buf[0], before[0]); + for i in 1 + len..N + 2 { + assert_eq!(buf[i], before[i]); + } + } + } + kani::cover(true, "rotate: all lengths and amounts up to 8 enumerated"); + } + + // ----------------------------------------------------------------------------------- + // Item 1: the drop-glue paths, for the `needs_drop` shape + // ----------------------------------------------------------------------------------- + + /// A `VecDeque` of capacity `<= 8` with `len <= N` elements written in place + /// (no destructor runs while building), symbolic head, and `DROPS` reset to zero. + fn small_deque_with_drop() -> VecDeque { + const CAP: usize = 8; + let requested: usize = kani::any(); + kani::assume(requested <= CAP); + let mut deque = VecDeque::::with_capacity(requested); + let cap = deque.capacity(); + kani::assume(cap <= CAP); + let head: usize = if cap == 0 { 0 } else { kani::any_where(|h: &usize| *h < cap) }; + let len: usize = kani::any_where(|l: &usize| *l <= cmp::min(cap, N)); + for i in 0..len { + unsafe { ptr::write(deque.ptr().add((head + i) % cap), WithDrop(kani::any())) }; + } + deque.head = head; + deque.len = len; + kani::cover(len > cap - head, "drop glue: wrapped layout"); + DROPS.store(0, Relaxed); + deque + } + + /// `truncate` runs the destructor of exactly the removed elements, and `Drop for + /// VecDeque` those of the remaining ones (`ptr::drop_in_place::<[T]>` on both slices). + #[kani::proof] + #[kani::unwind(10)] + fn bounded_truncate_drop_glue_withdrop() { + let mut deque = small_deque_with_drop(); + let len = deque.len(); + let new_len: usize = kani::any(); + deque.truncate(new_len); + let removed = len.saturating_sub(new_len); + assert_eq!(DROPS.load(Relaxed), removed); + assert_eq!(deque.len(), len - removed); + kani::cover(removed > 1 && len > removed, "truncate: several dropped, some remain"); + drop(deque); + assert_eq!(DROPS.load(Relaxed), len); + } + + /// `drain` runs the destructor of exactly the drained elements (the ones not pulled out + /// through `Drain`'s destructor), the rest through `Drop for VecDeque`. + #[kani::proof] + #[kani::unwind(10)] + fn bounded_drain_drop_glue_withdrop() { + let mut deque = small_deque_with_drop(); + let len = deque.len(); + let (start, end) = any_subrange(len); + let mut drain = deque.drain(start..end); + let pulled: bool = kani::any(); + if pulled { + if let Some(elem) = drain.next() { + drop(elem); + } + } + drop(drain); + assert_eq!(DROPS.load(Relaxed), end - start); + assert_eq!(deque.len(), len - (end - start)); + kani::cover( + pulled && end - start > 1 && start > 0 && end < len, + "drain: one pulled, interior range", + ); + drop(deque); + assert_eq!(DROPS.load(Relaxed), len); + } + + /// `Drop for VecDeque` runs every element's destructor exactly once, for both ring + /// layouts. + #[kani::proof] + #[kani::unwind(10)] + fn bounded_vecdeque_drop_glue_withdrop() { + let deque = small_deque_with_drop(); + let len = deque.len(); + let wrapped = len > deque.capacity() - deque.head; + drop(deque); + assert_eq!(DROPS.load(Relaxed), len); + kani::cover(wrapped && len > 1, "Drop for VecDeque: wrapped layout"); + } + + /// `retain_mut` drops exactly the rejected elements (through `truncate`), `Drop for + /// VecDeque` the kept ones. `retain_mut`'s own loops run under their loop contracts + /// here as everywhere; the drop glue is what this harness bounds. + #[kani::proof] + #[kani::unwind(10)] + fn bounded_retain_mut_drop_glue_withdrop() { + let mut deque = small_deque_with_drop(); + let len = deque.len(); + deque.retain_mut(|_| kani::any()); + let kept = deque.len(); + assert_eq!(DROPS.load(Relaxed), len - kept); + kani::cover(kept > 0 && kept < len, "retain_mut: some dropped, some kept"); + drop(deque); + assert_eq!(DROPS.load(Relaxed), len); + } + } + #[kani::proof] fn check_vecdeque_swap() { // The array's length is set to an arbitrary value, which defines its size.