Verify safety of Vec functions (Challenge 23)

[jrey8343]

Summary

Resolves #284

Adds Kani verification harnesses for 32 Vec functions listed in Challenge 23:

• from_raw_parts, into_raw_parts_with_alloc, into_boxed_slice, truncate, set_len, swap_remove, insert, remove, retain_mut, dedup_by, push, push_within_capacity, pop, append, append_elements, drain, clear, split_off, leak, spare_capacity_mut, split_at_spare_mut, extend_from_within, into_flattened, extend_with, deref, deref_mut, into_iter, extend_desugared, extend_trusted, extract_if, drop, try_from

Additionally verifies split_at_spare_mut_with_len (called transitively through split_at_spare_mut) and spec_extend_from_within (called transitively through extend_from_within).

Note: from_nonnull and from_nonnull_in are listed in the challenge but do not exist in this version of the codebase. All other 35 functions are verified.

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 by constructing from a fixed-size array then truncating to a symbolic length
• 128 total harnesses (32 per type × 4 types), all passing

Verification

./scripts/run-kani.sh --kani-args --harness verify_vec_ -p alloc --features alloc/kani

Test plan

• All 128 harnesses pass locally (u8: 33s, unit: 29s, char: 38s, tup: 39s)
• rustfmt applied
• CI passes

[jrey8343]

CI is passing — ready for review.