Challenge 24: verify Vec IntoIter and spec_* function safety with Kani

[kasimte]

TLDR: Kani harnesses for all 22 Challenge 24 targets (Vec::IntoIter + the spec_*/from_elem/extract_if helpers) — 26 harnesses verifying the real shipped bodies (no cfg(kani) rewrites) over symbolic-length inputs, with functional postconditions and ZST-arm coverage. Unbounded and generic-T are not literally met — the same committee question open across the sentence-pair challenges — and are disclosed below.

Towards #285.

Context

Challenge 24 covers the safety of Vec's consuming iterator IntoIter (library/alloc/src/vec/into_iter.rs) plus the specialization helpers it routes through (spec_extend, spec_from_iter, spec_from_iter_nested, spec_from_elem, extract_if). These read and advance a raw pointer pair (ptr/end) into a heap allocation, so the safety obligations are pointer in-bounds, no double-drop on early exit or panic, and correct handling of the ZST encoding (where end walks by bytes and ptr stays fixed).

Solution

26 harnesses across the 22 listed functions. Each exercises the function's actual shipped body — no #[cfg(kani)] body substitution and no kani::assume(false) on any real branch — and asserts the function's observable effect, not just the absence of UB.

• Symbolic-length inputs. Vecs are built at a symbolic length via kani::slice::any_slice_of_array + to_vec, so the pointer-walking loops (fold, try_fold, next/next_back, advance_by/advance_back_by) run a symbolic number of iterations up to the backing size (64 for the IntoIter harnesses; the allocation-heavy harnesses use smaller bounds, detailed under limitations).
• Functional postconditions. size_hint == (len, Some(len)); next/next_back return exactly the first/last element and shrink the remaining length by one; advance_by(k)/advance_back_by(k) return Ok iff k <= len, with the remaining length checked in both branches; next_chunk::<2> succeeds iff len >= 2; fold visits exactly len elements; from_elem(elem, n) produces length n with v[j] == elem at a symbolic index; spec_extend/from_iter preserve length and element values at a symbolic index; into_vecdeque preserves length.
• Early-exit and drop-glue paths are hit, not assumed. try_fold uses a comparator that can short-circuit (Err), in both a u8 variant and a Drop-carrying variant whose remaining elements are destroyed by IntoIter's real Drop — the double-drop class the body's ptr.add(1)-before-f ordering exists to prevent. drop and forget_allocation_drop_remaining also use the Drop-carrying type. extract_if::next reads and writes through the actual vec.as_mut_ptr().add(i) pointer (no can_write assumption).
• ZST arm covered. Every IntoIter method has a structurally separate T::IS_ZST branch (byte-walking end, fixed ptr); next/fold/advance_by are verified on Vec<()> at symbolic length, covering that distinct branch.
• Existing contract exercised. __iterator_get_unchecked already carries #[requires(i < self.len())] + kani::modifies(self) on main, previously with no exercising harness. Kani cannot resolve a generic trait-impl method as a proof_for_contract target (kani#1997), so the harness here is the mirroring assume-guarded proof, asserting the read's value against the source slice, with an in-code note.
• Non-vacuity witnessed. Every assume-bearing harness carries a satisfied kani::cover witness (12 covers total, including loop witnesses on the fold/drain harnesses).

How to verify

Scoped to these harnesses (from the repo root):

kani verify-std -Z unstable-options ./library -Z function-contracts -Z mem-predicates \
  -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts \
  --harness vec::into_iter::verify --harness vec::extract_if::verify \
  --harness vec::spec_extend::verify --harness vec::spec_from_elem::verify \
  --harness vec::spec_from_iter::verify --harness vec::spec_from_iter_nested::verify \
  --cbmc-args --object-bits 12

Expected: Complete - 26 successfully verified harnesses, 0 failures, 26 total. with 1 of 1 cover properties satisfied for each of the 12 covers. The harnesses also run in the standard ./scripts/run-kani.sh sweep, as in CI. (Verified locally at Kani 0.67.0 / CBMC 6.10.0.)

Reviewer notes — disclosed limitations

• Unbounded (arbitrary length): not literally met. All harnesses are length-bounded (64 for the IntoIter functions; smaller where noted below). We also measured a loop-contract route to genuine unboundedness on the IntoIter pointer loops: once the loop contract havocs the pointer, the invariant must re-establish pointer validity via kani::mem::same_allocation, and CBMC does not terminate on that predicate for these loops. A minimal same_allocation loop invariant over a stack array does verify, so the limit is specific to the IntoIter heap-pointer shape rather than the predicate in general; the index-based loop invariants used for the core iterators do not hit it. The bounded harnesses above are the working encoding today.
• Generic T: not met. Harnesses use representative element types (u8, () for the ZST arm, and a Drop-carrying token for drop glue). This is the same acceptance question open across the sentence-pair challenges; deferring to the committee on whether representative-type coverage satisfies the clause.
• Bounds on the allocation-heavy harnesses. extract_if::next (3) and the default from_iter (4) exceed the CI-standard --object-bits 12 object budget at larger sizes (measured); the Drop-token harnesses use a small fixed size (4) because drop obligations are per-element identical, so larger sizes add solver time without new proof obligations. Each bound is noted in-code at its site.
• Growth paths. The spec_extend harnesses pre-size the destination so append_elements' reserve is a no-op: the copy path is verified; element-by-element growth routes through extend_desugared (a Challenge 23 target) whose reallocation branch exceeds the object-bits budget above.
• Every changed line is additive (+496 / -0 across 6 files); no runtime logic is modified.