Challenge 23: verify Vec mod.rs function safety with Kani

[kasimte]

Towards #284.

Towards Challenge 23: Verify the safety of Vec functions part 1: Kani harnesses for all 36 listed public Vec functions in alloc::vec::mod, each exercising the function's real shipped body — no cfg(kani) substitution, no assume(false). Allocation and growth paths are verified over a symbolic, unbounded capacity; content and shift paths over a symbolic length. All 51 harnesses in vec::verify (the 50 added plus the pre-existing verify_swap_remove) pass via scripts/run-kani.sh.

Changes

File	Change
vec/mod.rs	50 harnesses added to the existing mod verify; safety::{requires,ensures} contracts on from_raw_parts, from_parts, from_parts_in, and set_len; a real safety::loop_invariant + loop_modifies on retain_mut's in-place loop
lib.rs	proc_macro_hygiene made an unconditional feature, mirroring core: retain_mut carries a statement-position #[safety::…] attribute in every build, so the gate cannot be cfg(kani)-only

Verification

Every harness runs the shipped body and asserts the observable effect. By approach:

Functions	Approach
push, push_within_capacity, spare_capacity_mut, split_at_spare_mut(_with_len), into_boxed_slice, into_raw_parts_with_alloc, append_elements, extend_trusted, extend_desugared grow path	Symbolic unbounded capacity: Vec::with_capacity(cap), cap free in 1..=isize::MAX/4, no length constant. Reallocation and growth run at symbolic capacity, not a fixed buffer
from_raw_parts, from_parts, from_parts_in, set_len	safety::{requires,ensures} verified with proof_for_contract (modifies(self) on set_len). The provenance/initialization obligations that are not expressible as predicates are documented at each contract; the proofs build valid parts (and, for set_len, pre-initialize the spare region before growth) rather than assuming them
insert, remove, truncate, retain, drain, extract_if, and the other content/shift functions	Symbolic length (bounded per function — see Scope) built with a loop-contract-free copy_nonoverlapping (the kani::vec::any_vec idiom); insert/remove snapshot a symbolic element and assert its post-shift position
retain_mut	Real-body loop_invariant + loop_modifies on the in-place critical-section loop. Loop contracts on the other in-place loops (extend_with, dedup_by) were measured non-convergent within CI at this pin, so those functions are bounded instead
push_within_capacity, set_len, swap_remove	Failure and edge arms: both push_within_capacity results, set_len's growth direction (spare region initialized first), and swap_remove's out-of-bounds panic as #[kani::should_panic]
insert, remove, truncate, swap_remove, retain, drain	Additionally run over a Drop type and an over-aligned type (#[repr(align(16))])

Wherever a harness restricts inputs with kani::assume, a kani::cover confirms the restriction is satisfiable: 48 covers against 29 assumes.

Scope

Allocation capacity is unbounded — growth runs at a free symbolic capacity. Two notes on the mandatory criteria:

• Element length is bounded per function. A symbolic-unbounded loop_modifies region overflows CBMC's write-set machinery at this pin, so each loop- or shift-bearing harness runs its real body at the largest length CBMC completes: 0..=64 for most, 0..=4 (a few 0..=2) where a shift or in-place loop dominates. Symbolic insert/copy offsets hit the same wall: a few harnesses fix the offset, values stay symbolic.
• Generic T (no monomorphization). A Kani harness is necessarily monomorphic, so this clause is not expressible in Kani; it is deferred to the committee. The harnesses instead span the element-type axes: size (u8), zero-size (Vec<()>), over-alignment (#[repr(align(16))]), and drop glue (a Drop type).

Every changed line is additive (+878/−0); the only annotations on shipped code are Kani-inert attributes. The spec's from_nonnull/from_nonnull_in are from_parts/from_parts_in in the current source.

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

[kasimte]

This PR adds #![feature(proc_macro_hygiene)] to alloc. It is required because retain_mut carries a bare #[safety::loop_invariant(...)] on its loop: an attribute macro in statement position must parse in all builds, not only under Kani. core enables the feature for the same reason; the attribute is inert outside Kani.