[kasimte]

Towards #285. Kani harnesses for Challenge 24: Verify the safety of Vec functions part 2.

47 harnesses cover all 22 listed functions — Vec::IntoIter (14) and the spec_* helpers it routes through (spec_extend, spec_from_iter/_nested, spec_from_elem, from_elem, extract_if). Each runs the real shipped body (no #[cfg(kani)] rewrite, no assume(false) on a real branch), at symbolic length where tractable, and asserts the observable effect, not just absence of UB. All pass via scripts/run-kani.sh at Kani 6ce55b9 / CBMC 6.11, with 29 kani::cover witnesses. Additive, +976/−0 across 7 files.

Spec requirement	Status
22 functions — no UB on the real body	all 22; functional postconditions asserted (e.g. advance_by(k) → Ok iff k <= len; fold visits exactly len)
__iterator_get_unchecked safety contract	real proof_for_contract at u8/Global and [u8; 3]/Global (Upstream below)
Drop / early-exit paths	hit, not assumed — try_fold short-circuits in a Drop variant (a double-drop would be caught); extract_if::next writes through the real pointer
Unbounded length	not met — length-bounded (64, smaller where noted); the loop-contract route is tool-walled (CBMC does not terminate on the same_allocation invariant the havoced heap-pointer loops need)
Generic T	representative, not parametric; open committee question (#734) — see below

Generic T (#734). On the size/align-branch axis the ruling asks about: IntoIter's 14 functions consume an already-built Vec and have no size_of/align_of-gated branch (nothing to reach). The one such branch in the spec_* callees (min_non_zero_cap) is reached at the size == 1 arm (Vec<u8>); its larger arms are reached only by growing through extend_desugared — a Challenge 23 function, not one of this challenge's 22, and object-bits-walled on its realloc path besides — disclosed in-code. Because element access is typed pointer arithmetic, representative types span the layout properties it depends on: u8, () (ZST), #[repr(align(16))], [u8; 3] (odd stride), and a Drop token.

Upstream Kani. __iterator_get_unchecked lives in a generic trait impl; naming the allocator explicitly resolves it as a proof_for_contract target via our merged fix kani#4865 (instantiate path generic arguments during type resolution). The harnesses verify its shipped #[requires(i < self.len())] + kani::modifies(self) contract directly.

Beyond fresh iterators, 13 harnesses re-check the surface from arbitrary reachable states — a symbolic number of elements consumed from each end via advance_by/advance_back_by, results checked against a pre-conversion snapshot.

Residual bounds, each noted in-code: extract_if::next and the default from_iter exceed --object-bits 12 at larger sizes; the Drop-token harnesses fix size 4 (per-element-identical obligations); element-by-element growth routes through Challenge 23's extend_desugared/extend_with, not claimed here.

Verify with scripts/run-kani.sh (standard -Z flags, --object-bits 12), scoped to the vec::{into_iter,extract_if,spec_*}::verify harnesses; 47 verified, 0 failures.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

Challenge 24 requires: "The verification must be unbounded---it must hold for slices of arbitrary length." That requirement is final. A Kani solution will only be accepted if it is unbounded in the input size for every required function. This PR still verifies at least part of the challenge with bounded harnesses (kani::unwind bounds and/or fixed-size inputs), so I'm requesting changes until every required function is verified without a bound on the input size.