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

[jrey8343]

Resolves #286 (Challenge 25). All changes are in library/alloc/src/collections/vec_deque/mod.rs (plus #![feature(proc_macro_hygiene)] in library/alloc/src/lib.rs, which is what lets #[safety::loop_invariant] sit on a statement, as in core/src/lib.rs; no runtime effect).

What is verified

• 13 unsafe functions with contracts (safety::{requires, ensures} + kani::modifies), each with #[kani::proof_for_contract] harnesses: push_unchecked, buffer_read, buffer_write, buffer_range, copy, copy_nonoverlapping, wrap_copy, copy_slice, write_iter, write_iter_wrapping, handle_capacity_increase, from_contiguous_raw_parts_in, abort_shrink; additionally rotate_left_inner / rotate_right_inner (unsafe fns on the safe list) carry contracts too.
• 30 safe abstractions with #[kani::proof] harnesses: get, get_mut, swap, reserve_exact, reserve, try_reserve_exact, try_reserve, shrink_to, truncate, as_slices, as_mut_slices, range, range_mut, drain, pop_front, pop_back, push_front, push_back, insert, remove, split_off, append, retain_mut, grow, resize_with, make_contiguous, rotate_left, rotate_right, rotate_left_inner, rotate_right_inner.

Unbounded. Every harness starts from any_deque(): a real allocation of symbolic capacity, a symbolic head over every valid physical index and a symbolic len (0..=cap), with exactly the logical range initialized. There is no kani::unwind and no length constant in any proof; the only assumption on sizes is Layout::array::<T>(cap).is_ok() (RawVec's own precondition) and cap * size_of::<T>() <= 2^48 (CBMC's object model under --object-bits 12, see MAX_ALLOCATION_BYTES). Loops are discharged with loop contracts (retain_mut's two shipped loops, and write_iter's iteration — see item 2 below).

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

Changes since the 2026-09-13 review

The three review items, in the reviewer's order. The 125 reviewed harnesses keep their bodies except for the plumbing listed under "Diff to the reviewed revision" (the two the reviewer reproduced locally, check_push_unchecked_u8 and check_write_iter_u8, are unchanged).

1. Generic T — representative shapes, with the properties VecDeque observes covered

Kani rejects #[kani::proof] on a generic function (attributes.rs: "the #[kani::proof] attribute cannot be applied to generic functions"), so each harness body is written once for arbitrary T and instantiated over element shapes. VecDeque<T> 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). The shapes now cover every one of those properties:

shape	size	align	needs_drop / non-Copy	validity invariant	instantiated on
()	0	1	no	no	every harness
u8	1	1	no	no	every harness
u64	8	8	no	no	every contract harness, the cheap safe ones
[u8; 3]	3	1	no	no	the cheap contract harnesses
bool (new)	1	1	no	yes (0/1)	push_unchecked, buffer_read, write_iter, get, pop_front, push_back
Al16 (new, #[repr(align(16))])	16	16	no	no	the cheap contract harnesses, get, pop_front, push_back, shrink_to, split_off
WithDrop (new, impl Drop with a destructor counter)	1	1	yes	no	every target that moves or reads elements and drops at most single ones: push_unchecked, buffer_read, buffer_write, write_iter, write_iter_wrapping, from_contiguous_raw_parts_in, get, get_mut, swap, pop_front, pop_back, push_front, push_back, remove, split_off, append

The generators write pre-existing elements with one symbolic byte per region — now a valid bit pattern of the shape (Shape::any_fill, which bool overrides), so they are sound for types with a validity invariant; elements that enter through the API are per-element kani::any(). What cannot be unbounded for a needs_drop shape is the slice drop glue: drop_in_place::<[T]> is a compiler-generated loop that cannot carry a loop contract, so truncate, drain, retain_mut (which truncates) and Drop for VecDeque are checked for WithDrop bounded (len <= 4) in verify::bounded_evidence, asserting through the counter that exactly the removed elements' destructors run, and every element's exactly once when the deque is dropped. Every other path is unbounded for all shapes.

This is the in-tool maximum; whether representative shapes satisfy the literal "no monomorphization" clause is the committee question the review names (see "Items requiring committee sign-off").

2. write_iter's cfg(kani) transcription — kept (it is the minimum at any current pin), what it hides now machine-checked

write_iter ships iter.enumerate().for_each(|(i, element)| unsafe { self.buffer_write(dst + i, element); *written += 1; }) under #[cfg(not(kani))] and runs the explicit loop write_iter_loop (loop contract) under #[cfg(kani)]. Three facts, each checked against the pinned Kani 152c6a8 (the pin main moved to on 2026-09-12; both spike errors below were reproduced at it):

• No unbounded proof of the literal for_each text exists at any current pin. The shipped loop is inside Iterator::for_each → Enumerate::fold → I::fold (core, library/core/src/iter/adapters/enumerate.rs, traits/iterator.rs), where no loop contract can be attached. A loop contract inside a harness iterator's own fold sits below Enumerate::fold, which moves its index count into a closure that the loop either havocs (it is a loop local; loop_modifies of a reference lowers to __CPROVER_object_whole) or writes in violation of the assigns clause — and no invariant can name a closure field. Stubbing Enumerate::fold (Kani Handle divide by zero in constant evaluator rust-lang/rust#4587, trait-method stubbing, is in the pin) is rejected because fold has method-level generics that the resolver does not pass; for_each is a non-overridden default (Kani doc: Document mutable function arguments rust-lang/rust#4588). Kani's own for-loop support is itself a rewrite to an indexed while (kani_macros/src/sysroot/loop_contracts/mod.rs, "types that cannot be havocked effectively … private fields").
• stub_verified(write_iter) is not available at the pin, and would not be enough. At 152c6a8, stub_verified on a contract whose modifies names a slice still ICEs (kani-compiler/src/kani_middle/reachability.rs:420: "Failed to resolve std::iter::IntoIterator::into_iter with &mut [[u8]]", Kani String concatenation with + only type-checks if the first operand is an owned pointer rust-lang/rust#3682; the fix auto: vim syntax highlighting improvements rust-lang/rust#4749 is 92 commits after the pin), and kani::stub of a contracted function still fails ("Failed to find contract closure __kani_recursion_check_abs_val", Kani Rewrite the coercion code to be more readable, more sound, and to reborrow when needed. rust-lang/rust#4591). Even with auto: vim syntax highlighting improvements rust-lang/rust#4749, a pure contract replacement would not prove write_iter_wrapping's wrapping branch: the generated replacement drops the by-value ByRefSized(&mut iter).take(head_room) unconsumed, so the second write_iter(0, iter, ..) sees the whole iterator again, havocs slots(0, n) outside write_iter_wrapping's modifies region and can push written past len; and iter is moved, so no ensures on write_iter can observe its post-state. The earlier PR text's "once the pin includes auto: vim syntax highlighting improvements rust-lang/rust#4749 this can become a plain stub_verified(write_iter)" was wrong and is withdrawn.
• What is now machine-checked about the transcription. The shipped statement is also compiled under Kani, byte for byte, as the sibling method write_iter_for_each ("must stay byte-identical; diff it"), and verify::bounded_evidence::bounded_write_iter_shipped_text_{u8,u64,u8x3,unit,withdrop} are proof_for_contract(write_iter) harnesses that substitute it for write_iter_loop — the shipped text checked against the same contract, the deque fully symbolic, the iterator length bounded by 4 (#[kani::unwind(6)]). The unbounded proof stays on the transcription (check_write_iter_*), whose doc now states what it relies on (Iterator's documented equivalence of fold and repeated next()), that loop-contract proofs are partial-correctness proofs at this pin (termination follows from the exact size_hint of TrustedLen iterators; loop_decreases cannot be combined with an explicit loop_modifies at this pin), and the future condition under which the transcription can move out of alloc (Kani gaining stubbing of generic trait methods, so that core's Enumerate::fold can be replaced).

Flagged for committee sign-off below, as requested.

3. The stubs — argument turned into checks; each stub's evidence in one table

replacement	replaces	asserts	over-approximates	evidence harness	residual argument
write_iter_loop (cfg(kani) body of write_iter)	the shipped for_each statement	—	— (transcription)	bounded_write_iter_shipped_text_*: the shipped statement against the same contract, n <= 4	fold ≡ repeated next()
VecDeque::write_iter_contract_replacement (callers of write_iter; _drop variant for resize_with, whose Take<RepeatWith<_>> cannot be advanced without a loop)	write_iter_loop	write_iter's precondition — through the same predicate the contract uses, write_iter_precondition, so the two cannot drift	the modifies region slots(dst, hi) gets an arbitrary valid fill; written += hi; iterator advanced by hi	bounded_write_iter_wrapping_shipped_text_u8 (the wrapping branch with the shipped statement iterating on the real Take<ByRefSized<&mut _>> stack: written == n) and bounded_replacement_advance_by_matches_next_u8 (advance_by(hi) ≡ hi × next() on that stack and on the bare iterator)	exact-hi = TrustedLen exactness (asserted lo == hi); a symbolic n <= hi would put the second call's havoc outside the caller's modifies, the same failure as above
stub_ptr_rotate (check_make_contiguous_*)	core::slice::rotate::ptr_rotate (pub(super) in core; no contract exists for it)	its documented precondition (the range is writable)	leaves memory untouched	bounded_rotate_permutes_range_u8: the real <[u8]>::rotate_left/rotate_right (the calls make_contiguous makes) on ranges of every length and amount up to eight, symbolic contents, symbolic guard bytes on both sides — the range holds exactly the rotated sequence, the guards are untouched (lengths and amounts enumerated so that only the selected, loop-free ptr_rotate_memmove is explored; the looping algorithms need min(left, right) > 256 for u8)	a rotation only permutes initialized slots; make_contiguous does nothing value-dependent afterwards

The replacement's doc comment is corrected: it writes exactly hi (the code always did; the comment said "some n ≤ hi"). Two things were tried and abandoned at the pin, recorded in the doc: running the real write_iter_loop inside resize_with and a direct-branch-only write_iter_wrapping harness (the loop contract is then instrumented for the Take<ByRefSized<&mut _>> instance too; neither finished within 20 minutes), a stub-free unbounded make_contiguous restricted to inputs whose rotation is the loop-free ptr_rotate_memmove (3.8 GB and unfinished after 20 minutes), and make_contiguous itself with the real rotation on an eight-slot buffer with symbolic layout (the unreachable looping algorithms of ptr_rotate are unwound anyway and the harness exceeded 17 GB).

bounded_evidence

None of the 12 harnesses in verify::bounded_evidence is the proof of a listed function; each is supplementary evidence for one stub, one transcription or one drop-glue path named in its doc comment, the module is the only place in verify that uses #[kani::unwind], and every listed function keeps its unbounded harness in the parent module. The write_iter iteration is exercised there through the contract-free write_iter_for_each, never through a loop that carries a loop contract (Kani would replace such a loop by its contract regardless of the unwind bound).

Items requiring committee sign-off

1. Representative shapes for generic T — machine-checked: every property the code observes, over the seven shapes above; argued: that these shapes stand for all T (parametricity of the code in T); the slice drop glue is bounded evidence only.
2. The write_iter transcription — machine-checked: the transcription unbounded (check_write_iter_*), the shipped text bounded (bounded_write_iter_shipped_text_*); argued: Iterator::fold ≡ repeated next(); why it cannot be otherwise at any current pin is derived above.
3. The stubs — the evidence table above; residual arguments in its last column.

Diff to the reviewed revision

• Upstream sync: main merged (toolchain nightly-2026-02-05, Kani pin 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 ("Cannot stub VecDeque::<T, A>::write_iter_loop … Expected type &mut VecDeque<T, A> for parameter 1, but found &mut VecDeque<T, A>"); the replacement is therefore now a #[cfg(kani)]-only sibling method (VecDeque::write_iter_contract_replacement), which is the only change needed for the reviewed revision to build at the new pin.
• Production side (attributes and #[cfg(kani)] items only): write_iter's #[requires] now calls write_iter_precondition; new write_iter_precondition, write_iter_for_each; doc rewrites on write_iter/write_iter_loop.
• mod verify: module documentation (method, shape matrix, evidence table, pinned-Kani limitations); Shape trait with the fill hook, the three new shapes, finish() (leaks the deque for needs_drop shapes, drops it otherwise); the eight let _ = ptr::read(..) alias-drop sites became mem::forget(ptr::read(..)) (a bitwise copy of a live element must not run a destructor); finish(deque) at the end of the 16 harnesses instantiated with WithDrop; T: Shape bounds; the replacement renamed and moved as described; new instantiation lines; bounded_evidence.

Local results

Pinned Kani 152c6a8 (the pin CI uses since #613), CBMC 6.10.0, CI's flags (-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12): 172 of 172 harnesses verified, 0 failures, all 918 kani::cover witnesses SATISFIED. Sequential run (one harness at a time, full output): 53 min 35 s wall including the library build, 42.5 min of CBMC time in total — 32.2 min for the 125 reviewed harnesses (heaviest: check_wrap_copy_u64 107 s, check_copy_u8x3 101 s, check_wrap_copy_u8 99 s, check_insert_u8 92 s), 10.3 min for the 47 added ones (heaviest: bounded_rotate_permutes_range_u8 180 s, bounded_write_iter_shipped_text_u8x3 64 s; the 34 new shape instantiations average 6 s). Parallel run (-j, 12 cores): 12 min 12 s wall. Reports: the loop-invariant base/step checks appear in check_write_iter_* and check_retain_mut_* only; among the bounded harnesses only bounded_retain_mut_drop_glue_withdrop carries loop-contract instrumentation (its retain_mut loops, by design); the replacement's checks are visible by name in the reports of its callers (write_iter precondition, write_iter callers pass TrustedLen iterators, write_iter replacement: iterator advanced by hi).

🤖 Generated with Claude Code

https://claude.ai/code/session_01XjuqtSUTkxA5kjmq32PEoJ

[feliperodri]

Thanks @jrey8343 — and apologies this was missed in the first Challenge 25 round (created after our triage snapshot). Reviewed now with our vacuity tooling + local Kani (pinned 0.67.0 / CBMC 6.8.0).

This is by far the strongest Challenge 25 submission and a genuine breakthrough: the first TRULY UNBOUNDED VecDeque solution. any_deque allocates a symbolic cap constrained only by Layout::array::<T>(cap).is_ok() + the CBMC object-model bound — no kani::unwind, no MAX_LEN, no length constant anywhere, both contiguous and wrapped ring layouts covered. A real advance over #564/#605 (both bounded). 13/13 unsafe fns with genuine #[requires]/#[ensures] + #[kani::proof_for_contract] and 30/30 safe abstractions. It even surfaced a real upstream unsoundness (rust-lang#162452). Clean soundness elsewhere: substantive ring invariant_holds() (not true), real loop invariants, no orphan contracts, no kani::assume(false), and — unlike #605 — no out-of-scope core:: edits.

Local Kani (CBMC 6.8.0): check_push_unchecked_u8 (unbounded proof_for_contract) and check_write_iter_u8 (the loop-contract harness) both VERIFICATION SUCCESSFUL. The unbounded harnesses are CBMC-heavy (wrap_copy didn't finish in ~10 min locally) — relevant to the "completes within CI resource limits" bar; please confirm the full suite is green in CI.

Requesting changes on the items to resolve before acceptance:

1. Generic-T. Bodies are generic (fn check_x<T: kani::Arbitrary>()) but instantiated over representative types (u8/u64/[u8;3]/()). Kani requires monomorphized harnesses, so literal "no monomorphization" is unachievable in-tool — the same open question across Ch16/17/18/23/24. Needs a committee ruling on whether representative-type coverage satisfies the clause; until then I can't mark it as literally meeting the criterion (for consistency with those challenges).
2. write_iter cfg(kani) loop-paraphrase (T1). #[cfg(not(kani))] ships the real for_each; #[cfg(kani)] runs write_iter_loop. Runtime is unchanged and the paraphrase is a faithful transcription (justified by kani#4591/rust-lang#3682/rust-lang#4749) and verified locally — but the proof runs the paraphrase, not the shipped body. Move to the stub_verified path once the pin includes rust-lang#4749, and flag for committee sign-off.
3. Three hand-written stubs (model_write_iter, stub_write_iter_loop(_drop), stub_ptr_rotate) are modular over-approximations whose soundness rests on argument — principled and documented, but reviewer trust points.

This is the prioritized Ch25 solution and the closest any unbounded-clause challenge has come to acceptance. If the committee accepts representative-mono generic-T and signs off on the write_iter paraphrase + stubs, this is approvable. Outstanding work.

[jrey8343]

Thanks for the review. The branch is synced to main (toolchain nightly-2026-02-05, Kani pin 152c6a8, CBMC 6.10.0) and re-verified at that pin; the PR description is rewritten to match. On the three items:

1. Generic T. In-tool the clause cannot be met literally (#[kani::proof] on a generic function is rejected), so I have done the next best thing and made the coverage argument precise: VecDeque<T> observes T only through size_of/align_of, T::IS_ZST, moves, and the slice drop glue in truncate/drain/Drop (it never branches on needs_drop or on values). The shapes now cover each of those: (), u8, [u8; 3], u64 as before, plus bool (validity invariant — the generators now write a valid bit pattern of the shape, so they are sound for such types), Al16 (#[repr(align(16))]) and WithDrop (needs_drop, non-Copy, destructor counter) on the targets that exercise them. The slice drop glue (drop_in_place::<[T]>, a compiler-generated loop that cannot carry a loop contract) is the one thing that stays bounded: truncate, drain, retain_mut and Drop for VecDeque are checked for WithDrop at len <= 4, asserting that exactly the removed elements' destructors run. The shape matrix and the exclusions are in the module doc and the PR. Status: representative shapes — requires the committee ruling you mention.

2. write_iter transcription (T1). Checked at 152c6a8 rather than assumed: kani::stub of a contracted fn still fails ("Failed to find contract closure __kani_recursion_check_…", kani#4591), and stub_verified on a slice-modifies contract still ICEs (reachability.rs:420, "Failed to resolve IntoIterator::into_iter with &mut [[u8]]", kani#3682 — auto: vim syntax highlighting improvements rust-lang/rust#4749 is 92 commits after the pin). More importantly, auto: vim syntax highlighting improvements rust-lang/rust#4749 alone would not discharge the wrapping branch of write_iter_wrapping: the generated replacement drops the by-value ByRefSized(&mut iter).take(head_room) unconsumed, so the second write_iter(0, iter, ..) sees the whole iterator again and the caller's own modifies/ensures fail — and iter is moved, so no ensures on write_iter can say it was consumed. I have withdrawn the earlier "becomes a plain stub_verified once auto: vim syntax highlighting improvements rust-lang/rust#4749 lands" sentence. Nor can the loop contract reach the shipped loop from below: it lives in Enumerate::fold, whose index is a closure local that a loop contract can neither name nor re-pin (derivation with file:line in the PR). What the swap hides is now machine-checked: the shipped statement is compiled under Kani byte for byte as a sibling method (write_iter_for_each, "diff it") and bounded_evidence::bounded_write_iter_shipped_text_{u8,u64,u8x3,unit,withdrop} check it against write_iter's contract with the deque fully symbolic and the iterator length bounded by 4. Status: swap kept as the minimum at any current pin, what it hides bounded-checked — flagging for committee sign-off as you suggested.

3. Stubs. Each is now in one table (PR and module doc): what it replaces, what it asserts, what it over-approximates, the harness that checks what it hides, the residual argument. stub_write_iter_loop/model_write_iter are one method, write_iter_contract_replacement, which asserts the precondition through the very predicate the contract uses (write_iter_precondition, so they cannot drift), havocs the modifies expression itself, and has its one step beyond the contract — consuming the iterator by exactly hi — checked two ways: bounded_write_iter_wrapping_shipped_text_u8 runs the wrapping branch with the shipped statement iterating on the real Take<ByRefSized<&mut _>> stack, and bounded_replacement_advance_by_matches_next_u8 checks advance_by(hi) ≡ hi × next() on that stack. (Its doc said "some n ≤ hi"; the code always wrote exactly hi, which the doc now says and justifies.) stub_ptr_rotate gets bounded_rotate_permutes_range_u8: the real rotate_left/rotate_right (the calls make_contiguous makes) on ranges of every length and amount up to eight with symbolic contents and guard bytes — exactly the rotated sequence, nothing else written. Two attempts to remove stub uses altogether did not converge at the pin and are recorded in the docs (the real write_iter loop inside resize_with/write_iter_wrapping's direct branch; a stub-free unbounded make_contiguous on the memmove-rotation class). Status: bounded-checked, arguments documented.

Bounded harnesses live in verify::bounded_evidence (named bounded_*, the only #[kani::unwind] users, disclaimed as non-proofs in the module doc); every listed function keeps its unbounded harness. Also from the sync: at 152c6a8 Kani rejects a free function as the stub of a method (signatures are compared by the position of their own generic parameters), so the replacement had to become a sibling method — the only change the reviewed revision needed to build at the new pin.

CI: the previous run (at the old merge ref) was green on all four verification partitions, metrics and autoharness; this push runs at the new pin and I will follow up here if anything fails. Local: 172/172 harnesses verified at the new pin, all 918 covers satisfied; 42.5 min of CBMC time sequentially (32.2 min for the 125 reviewed harnesses, 10.3 min for the 47 added ones, heaviest bounded_rotate_permutes_range_u8 at 180 s), 12 min wall with -j.