Challenge 24: Verify Vec Part2 safety with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Vec iterator-related functions in library/alloc/src/vec/ for Challenge 24: Verify the safety of Vec functions part 2.

The change introduces:

• a safety contract for IntoIter::__iterator_get_unchecked
• proof harness modules under #[cfg(kani)] for all Challenge 24 listed Vec iterator entries
• reusable symbolic Vec helpers for allocated, ZST, unbounded, and reserve-sensitive cases
• Kani loop contracts and Kani-only loop structure for IntoIter::fold, IntoIter::try_fold, ExtractIf::next, and Vec::extend_desugared

Verification Coverage Report

Coverage: 22 / 22 Challenge 24 entries targeted

IntoIter coverage includes:

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

Additional Vec iterator-path coverage includes:

• ExtractIf::next
• SpecExtend::spec_extend for IntoIter
• SpecExtend::spec_extend for slice::Iter
• SpecFromElem::from_elem for i8
• SpecFromElem::from_elem for u8
• SpecFromElem::from_elem for ()
• SpecFromIter::from_iter
• SpecFromIterNested::from_iter default path

Approach

The verification strategy combines executable harnesses with targeted contracts and loop annotations:

1. Add a precondition contract for IntoIter::__iterator_get_unchecked requiring the unchecked index to be within the iterator's remaining range.
2. Add #[kani::proof] harnesses for each Challenge 24 target, using symbolic Vec construction across integer types, usize/isize, unit/ZSTs, and arrays.
3. Add Kani loop invariants and modifies sets for iterator loops that move, drop, or write elements through raw pointers.
4. Model ZST and non-ZST iterator behavior separately where the implementation uses different pointer encodings.
5. Keep verification-only helper logic under cfg(kani).

Scope assumptions

• Generic T is represented through a broad set of concrete instantiations used by the harness macros.
• The __iterator_get_unchecked harness enforces the contract precondition directly because Kani currently cannot resolve the generic trait method target for proof_for_contract.

Verification

All added Challenge 24 harnesses pass locally with Kani.

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.