Challenge 23: Verify Vec Part1 safety with Kani

[v3risec]

Summary

This PR adds Kani-based verification artifacts for Vec APIs in library/alloc/src/vec/mod.rs for Challenge 23.

The change introduces:

• Kani contracts for unsafe raw reconstruction, length mutation, append, and spare-capacity splitting APIs
• proof harness modules under #[cfg(kani)] for all Challenge 23 listed Vec entries
• reusable symbolic Vec helpers for allocated, ZST, bounded, and reserve-sensitive cases
• Kani loop contracts and Kani-only loop structure for retain, dedup, extend, and trusted-iterator paths

No non-verification runtime behavior is changed in normal builds.

Notes on Challenge 23 Function Signatures

Several Challenge 23 names do not exactly match the current repository source. This PR follows the checked-in API definitions.

Notable alignments include:

• from_nonnull is verified as Vec::from_parts, the current NonNull<T> raw-parts constructor.
• from_nonnull_in is verified as Vec::from_parts_in.
• Internal listed entries such as append_elements, split_at_spare_mut_with_len, extend_with, spec_extend_from_within, extend_desugared, and extend_trusted are verified from inside vec::mod, where those private paths are accessible.

Verification Coverage Report

Coverage: 36 / 36 Challenge 23 entries targeted

Contract-backed unsafe/API groups include:

• Vec::from_raw_parts
• Vec::from_parts
• Vec::from_parts_in
• Vec::set_len
• Vec::append_elements
• Vec::split_at_spare_mut_with_len

Harness-backed coverage includes:

• raw-parts decomposition and boxed-slice conversion
• length and element operations: truncate, swap_remove, insert, remove, push, push_within_capacity, pop, clear
• bulk and iterator-related operations: append, drain, split_off, extend_from_within, extend_with, spec_extend_from_within, extend_desugared, extend_trusted, extract_if
• spare-capacity APIs: spare_capacity_mut, split_at_spare_mut, split_at_spare_mut_with_len
• trait paths: Deref, DerefMut, IntoIterator, Drop, and [T; N]::try_from(Vec<T>)
• panic-path harnesses for representative out-of-bounds and capacity-overflow cases

Approach

The verification strategy combines function contracts with executable harnesses:

1. Add kani::requires, kani::ensures, and kani::modifies clauses for unsafe pointer/length APIs where the source safety requirements can be expressed.
2. Add #[kani::proof_for_contract] harnesses for contract targets and #[kani::proof] harnesses for safe and internal APIs.
3. Use representative concrete instantiations across integer types, usize/isize, unit/ZSTs, fixed arrays, nested arrays, and a clone-only type.
4. Add Kani loop invariants and modifies sets for paths that manipulate initialized prefixes, spare capacity, and panic-safe length guards.
5. Keep verification-only helper accessors in SetLenOnDrop under cfg(kani) so normal builds preserve the original behavior.

Scope assumptions

• Generic T is represented through a broad set of concrete instantiations used by the harness macros.
• Raw pointer provenance is constrained with Kani memory predicates where currently expressible.

Verification

All added Challenge 23 harnesses pass locally with Kani.

Resolves #284

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