Challenge 23: Verify safety of Vec functions part 1

[Samuelsills]

Summary

Add Kani proof harnesses for all 36 Vec functions specified in Challenge #23:

from_raw_parts, from_nonnull, from_nonnull_in, 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, split_at_spare_mut_with_len, extend_from_within, into_flattened, extend_with, spec_extend_from_within, deref, deref_mut, into_iter, extend_desugared, extend_trusted, extract_if, drop, try_from

All harnesses verified locally with Kani.

Resolves #284

[Samuelsills]

Verification Coverage Report

Functions Verified (36/36 ✅)

from_raw_parts, from_nonnull (→from_parts), from_nonnull_in (→from_parts_in), 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, split_at_spare_mut_with_len, extend_from_within, into_flattened, extend_with, spec_extend_from_within, deref, deref_mut, into_iter, extend_desugared, extend_trusted, extract_if, drop, try_from

UBs Checked (automatic via Kani/CBMC)

• ✅ Accessing dangling or misaligned pointers
• ✅ Reading from uninitialized memory
• ✅ Mutating immutable bytes
• ✅ Producing an invalid value

Verification Approach

• Tool: Kani Rust Verifier
• 36 proof harnesses, one per spec function
• Note: spec names from_nonnull/from_nonnull_in map to source names from_parts/from_parts_in

[Copilot]

Pull request overview

Adds a Kani verification module (#[cfg(kani)] mod verify) in alloc::vec with proof harnesses covering a large set of Vec APIs as part of Challenge #23 (pointer arithmetic / safety validation).

Changes:

• Reworked the existing verify_swap_remove harness to a simpler bounds-checked index + postcondition.
• Added many new Kani proof harnesses for additional Vec methods (mutation, raw parts conversions, iteration, spare capacity APIs, etc.).
• Introduced a Vec::leak harness that attempts to reclaim leaked memory for verification runs.

[Copilot]

verify_leak attempts to “unleak” the returned slice by converting &mut [i32] into Box<[i32]> via Box::from_raw. This deallocation is only sound if the Vec’s allocation has no excess capacity (i.e., capacity == len) and uses the global allocator; otherwise the dealloc layout can mismatch the original allocation, which is UB. Prefer not deallocating here (accept the leak in the harness), or restructure the harness to avoid Vec::leak cleanup via Box::from_raw (e.g., only perform such cleanup when you can guarantee capacity == len).

Suggested change

	unsafe {
	drop(crate::boxed::Box::from_raw(leaked as *mut [i32]));
	}

[Copilot]

Several harnesses in this #[cfg(kani)] module call Vec APIs that are themselves #[cfg(not(no_global_oom_handling))] (e.g., push, reserve, insert, into_boxed_slice, extend_from_within, append). Under a build that enables no_global_oom_handling together with kani, these harnesses won’t compile because those methods are not available. Consider adding matching #[cfg(not(no_global_oom_handling))] gates to the affected proof functions (or otherwise gating the whole verify module) so cfg combinations remain buildable.