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) — 34 harnesses verifying the real shipped bodies (no cfg(kani) rewrites) over symbolic-length inputs, with functional postconditions, ZST-arm coverage, and element-type shape coverage (alignment, stride, validity, drop). 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

34 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 (14 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 - 34 successfully verified harnesses, 0 failures, 34 total. with 1 of 1 cover properties satisfied for each of the 14 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.)

Additional element-type shape coverage

The existing per-type harnesses are unchanged. This adds 8 harnesses extending
coverage to properties of T the current u8/i8/() instantiations do not
exercise. Values and lengths stay symbolic; each new harness body is written
once for arbitrary T and instantiated per shape.

added harness	method	property covered
check_into_iter_next_al16	next	over-alignment (#[repr(align(16))]): allocation + 16-byte stride
check_into_iter_next_bool	next	validity invariant (see note)
check_into_iter_next_droptoken	next	forward move-out of a destructor type
check_into_iter_next_back_droptoken	next_back	backward move-out drop (distinct geometry)
check_into_iter_get_unchecked_arr3	__iterator_get_unchecked	odd (non-power-of-two) stride indexed add(i); T: NonDrop is the trait's own bound
check_spec_extend_intoiter_droptoken	spec_extend (IntoIter)	bulk-move + forget_remaining_elements without double-drop
check_from_iter_intoiter_droptoken	SpecFromIter (IntoIter)	ManuallyDrop + from_parts ownership transfer
check_extract_if_next_droptoken	ExtractIf::next	leak-amplification backshift-on-drop

Shapes: a #[repr(align(16))] wrapper (Al16), [u8; 3] (odd stride), bool
(validity niche), and a destructor type (DropToken, with a real Drop impl so
needs_drop() is true) applied across the move/consume paths. Each new body
mirrors its existing _u8 counterpart with the element type swapped, so a green
result is a genuine property check, not a tautology. These shapes exercise drop
glue, validity-niche preservation, over-alignment, and odd (non-power-of-two)
stride for the element type — behaviour the u8/i8/() instantiations cannot
reach.

On bool and validity: kani::any::<bool>() yields only valid bit patterns,
so this harness proves the move-only element handling preserves a niche type's
validity invariant (the code never fabricates a bool from arbitrary bits) —
reading uninitialised memory as any T is caught by Kani's memory model
independently of the element type.

On the generic-T clause: this PR keeps its existing per-type harnesses and
adds shape coverage in generic-body form for the new instantiations. Full
conversion of the whole suite to single generic bodies is deferred pending the
committee ruling on the clause — we would rather not churn a verified suite
before the Option-A form is confirmed as the standard, and will complete the
conversion promptly on a favorable ruling.

CI cost

The 8 added harnesses each verify VERIFICATION:- SUCCESSFUL at the pinned
Kani (152c6a8, kani 0.67) / CBMC 6.10.0, object-bits 12, --no-assert-contracts
(CI-faithful, run-kani.sh). CBMC solving times: 2.7–15.5 s each, ≈57 s summed.

Exclusions (unchanged from the original submission)

• SpecFromElem's generic T: Clone default impl routes through extend_with
  (a Challenge 23 target); not claimed.

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, a Drop-carrying token for drop glue, and the over-aligned, odd-stride, and validity-niche shapes described under Additional element-type shape coverage above). 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 (+687 / -0 across 7 files); no runtime logic is modified.