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

[kasimte]

Towards #284. Solves 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 48 harnesses in vec::verify (the 47 added plus the pre-existing verify_swap_remove) pass via scripts/run-kani.sh.

Changes

File	Change
vec/mod.rs	47 harnesses added to the existing mod verify; safety::{requires,ensures} contracts on from_raw_parts, from_parts, 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, from_parts_in, 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, 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 genuinely-valid parts and pre-initialize the spare region 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 an over-aligned type (#[repr(align(16))]), a Drop type, and the ZST arm (Vec<()>)

Wherever a harness restricts inputs with kani::assume, a kani::cover confirms the restriction is satisfiable — 46 covers against 29 assumes — so no proof passes while checking nothing.

Scope

Allocation capacity is genuinely unbounded — the allocation and growth paths run at a free symbolic capacity, not a fixed buffer. Two notes on the mandatory criteria:

• Element length is bounded per function, for CI cost. Where a symbolic length drives an in-place shift or a loop_modifies region, an unbounded region overflows CBMC's write-set machinery and the shift/copy cost grows superlinearly, so each such harness takes the largest length that completes within CI resource limits: most content functions at 0..=64, the shift-heavy and loop-bearing ones lower (to 0..=4), each bound justified in-code. A symbolic insert/copy offset is likewise CBMC-prohibitive for a few harnesses, which fix the shape and keep the values 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 that matter for these functions: size (u8), zero-size (Vec<()>), over-alignment (#[repr(align(16))]), and drop glue (a Drop type).

Every changed line is additive (+842/−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]

Pre-verified on 7864d6c91c5 (this branch, on my fork's CI):

• All Kani jobs green — 8 verify-std partitions (both OSes), both autoharness jobs, and the analyzer.
• Cover satisfaction (report-only at this pin, so a green run does not by itself assert it): 932/932 cover properties satisfied across the run, 0 mismatches.

The upstream-only jobs the fork CI cannot run — build (full ./x build), upstream_test (./x fmt --check), check-flux-on-core, simd — are running here now. build exercises the one non-additive-looking line: proc_macro_hygiene is now an unconditional crate feature (a statement-position #[safety::…] attribute is present in all builds), mirroring core.