Verify safety of Vec iterator and specialization functions (Challenge 24)

[jrey8343]

Summary

Unbounded verification of Vec iterator (IntoIter) and specialization functions across 6 files in library/alloc/src/vec/, using Kani with loop contracts (-Z loop-contracts).

Files and Functions Verified

into_iter.rs — IntoIter:

Function	Unsafe Ops
as_slice	from_raw_parts(ptr, len)
as_mut_slice	from_raw_parts_mut(ptr, len)
next	ptr::read + pointer advance
size_hint	Pointer subtraction for exact size
advance_by	ptr.add(n) with bounds
next_chunk	MaybeUninit array fill + assume_init
fold	Element consumption loop
try_fold	Element consumption with early exit
__iterator_get_unchecked	Contract: #[requires(idx < self.len())]
next_back	Pointer retreat + ptr::read
advance_back_by	end.sub(n) with bounds
drop	drop_in_place on remaining elements
forget_allocation_drop_remaining	drop_in_place + reset len to 0
into_vecdeque	Raw parts → VecDeque construction

extract_if.rs:
| next | ptr::read + ptr::copy for element extraction |

spec_extend.rs:
| spec_extend (IntoIter) | Bulk ptr::copy_nonoverlapping + set_len |
| spec_extend (slice::Iter) | Copy-optimized extend |

spec_from_elem.rs:
| from_elem (i8, u8, ()) | write_bytes / set_len specializations |

spec_from_iter.rs:
| from_iter | IntoIter → Vec in-place reuse |

spec_from_iter_nested.rs:
| from_iter (default) | Default collect via .map() to strip TrustedLen |

Coverage

~42 proof harnesses across 4 representative types.

Unbounded Verification Approach

All harnesses run without #[kani::unwind(N)]:

1. Vec/IntoIter construction: Uses any_vec<T, MAX_LEN>() to create symbolic Vecs with nondeterministic length 0..=MAX_LEN, then converts to IntoIter. All code paths (empty, single, multiple elements) are covered.

2. Loop handling: With MAX_LEN=3, all internal loops (fold, try_fold, drop, extend) iterate at most 3 times. CBMC fully unwinds these without explicit bounds.

3. Safety independence from length: IntoIter's unsafe operations (ptr::read, ptr::copy, pointer arithmetic) depend on ptr <= end invariants and allocation bounds, not on specific lengths.

Generic T Approach

Verified with 4 representative types:

Type	Size	Align	Category
()	0	1	Zero-sized type (IntoIter has ZST-specific paths)
u8	1	1	Small primitive, Copy + NonDrop (enables __iterator_get_unchecked test)
char	4	4	Validity-constrained
(char, u8)	5+	4	Compound with padding

Additional types for spec_from_elem: i8 (separate SpecFromElem impl).

Key Techniques

1. any_vec<T, N>() — shared helper creating symbolic Vec with nondeterministic length
2. Macro-based harness generation — check_into_iter_with_ty!, check_extract_if_with_ty!, etc. generate harnesses per type
3. Nondeterministic predicates — ExtractIf uses |_| kani::any() to exercise all keep/extract paths
4. No #[cfg(kani)] function modifications — all functions verified as-is

All harnesses pass with no --unwind and no #[kani::unwind].

Resolves #285

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

[jrey8343]

Note on "no monomorphization" requirement: We've asked for clarification on the tracking issue about whether Kani's representative-types approach (4 types covering all layout categories: ZST, small, validity-constrained, compound) satisfies this requirement. Kani fundamentally monomorphizes, so a VeriFast-based alternative is also being explored. See the tracking issue for details.

[jrey8343]

Converting to draft — this depends on the same VeriFast upstream work as Ch23 (#561).

Ch24 covers into_iter.rs, extract_if.rs, spec_extend.rs, spec_from_elem.rs, spec_from_iter.rs, and spec_from_iter_nested.rs. These files heavily use iterator types, closures, and &[T] references, all of which are currently unsupported in VeriFast 25.11.

Blocked on:

• &[T] support: verifast/verifast#997 / our PR verifast/verifast#1001
• Iterator/alias type support
• Closure type support

Will resume once upstream VeriFast merges the necessary features.