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

[jrey8343]

Summary

Resolves #285

Adds Kani verification harnesses for all 21 Vec iterator and specialization functions listed in Challenge 24, across 6 files:

into_iter.rs (13 IntoIter functions):

• as_slice, as_mut_slice, next, size_hint, advance_by, next_chunk, fold, try_fold, __iterator_get_unchecked, next_back, advance_back_by, drop, forget_allocation_drop_remaining, into_vecdeque

extract_if.rs (1 function):

• ExtractIf::next

spec_extend.rs (2 specializations):

• spec_extend for IntoIter
• spec_extend for slice::Iter

spec_from_elem.rs (3 specializations):

• from_elem for i8, u8, ()

spec_from_iter.rs (1 specialization):

• from_iter for IntoIter

spec_from_iter_nested.rs (1 specialization):

• from_iter (default impl)

Approach

• Bounded verification with #[kani::unwind(8)] for loop-containing functions, MAX_LEN=3 arrays
• Generic verification via 4 representative types: u8, (), char, (char, u8) — no monomorphization
• Helper function any_vec<T, MAX_LEN>() creates symbolic Vec instances
• 83 total harnesses, all passing

Verification

# IntoIter harnesses (56)
./scripts/run-kani.sh --kani-args --harness verify_into_iter_ -p alloc --features alloc/kani

# ExtractIf harnesses (4)
./scripts/run-kani.sh --kani-args --harness verify_extract_if -p alloc --features alloc/kani

# SpecExtend harnesses (8)
./scripts/run-kani.sh --kani-args --harness verify_spec_extend -p alloc --features alloc/kani

# SpecFromElem harnesses (3)
./scripts/run-kani.sh --kani-args --harness check_from_elem -p alloc --features alloc/kani

# SpecFromIter harnesses (8)
./scripts/run-kani.sh --kani-args --harness verify_spec_from_iter -p alloc --features alloc/kani

# SpecFromIterNested harnesses (4)
./scripts/run-kani.sh --kani-args --harness verify_from_iter_nested -p alloc --features alloc/kani

Test plan

• All 83 harnesses pass locally
• rustfmt applied
• CI passes