Skip to content

Challenge 23: Verify safety of Vec functions part 1 #569

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Samuelsills wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Challenge 23: Verify safety of Vec functions part 1 #569

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
89e1b92
Challenge 23: Verify safety of Vec functions part 1
Samuelsills Mar 26, 2026
de85d5c
Fix formatting to match CI rustfmt expectations
Samuelsills Mar 26, 2026
79ccacf
Fix remaining rustfmt formatting issues
Samuelsills Mar 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
331 changes: 308 additions & 23 deletions library/alloc/src/vec/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4317,37 +4317,322 @@ mod verify {

#[kani::proof]
pub fn verify_swap_remove() {
// Creating a vector directly from a fixed length arbitrary array
let mut arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut vect = Vec::from(&arr);
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let i: usize = kani::any_where(|x| *x < v.len());
let _ = v.swap_remove(i);
assert!(v.len() == ARRAY_LEN - 1);
}

// Recording the original length and a copy of the vector for validation
let original_len = vect.len();
let original_vec = vect.clone();
#[kani::proof]
pub fn verify_push() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.push(kani::any());
assert!(v.len() == ARRAY_LEN + 1);
}
Comment on lines +4327 to +4333
Copy link

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copilot uses AI. Check for mistakes.

// Generating a nondeterministic index which is guaranteed to be within bounds
let index: usize = kani::any_where(|x| *x < original_len);
#[kani::proof]
pub fn verify_pop() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
assert!(v.pop().is_some());
assert!(v.len() == ARRAY_LEN - 1);
}

let removed = vect.swap_remove(index);
#[kani::proof]
pub fn verify_push_within_capacity() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.reserve(1);
assert!(v.push_within_capacity(42).is_ok());
}

// Verifying that the length of the vector decreases by one after the operation is performed
assert!(vect.len() == original_len - 1, "Length should decrease by 1");
#[kani::proof]
pub fn verify_insert() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let i: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
v.insert(i, 42);
assert!(v.len() == ARRAY_LEN + 1);
assert!(v[i] == 42);
}

// Verifying that the removed element matches the original element at the index
assert!(removed == original_vec[index], "Removed element should match original");
#[kani::proof]
pub fn verify_remove() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let i: usize = kani::any_where(|&x: &usize| x < ARRAY_LEN);
let _ = v.remove(i);
assert!(v.len() == ARRAY_LEN - 1);
}

// Verifying that the removed index now contains the element originally at the vector's last index if applicable
if index < original_len - 1 {
assert!(
vect[index] == original_vec[original_len - 1],
"Index should contain last element"
);
#[kani::proof]
pub fn verify_clear() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.clear();
assert!(v.is_empty());
}

#[kani::proof]
pub fn verify_truncate() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
v.truncate(n);
assert!(v.len() == n);
}

#[kani::proof]
pub fn verify_deref() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let v = Vec::from(&arr);
let s: &[i32] = &*v;
assert!(s.len() == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_deref_mut() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let s: &mut [i32] = &mut *v;
s[0] = 42;
assert!(s[0] == 42);
}

#[kani::proof]
pub fn verify_leak() {
let v = Vec::from(&[1i32, 2, 3]);
let leaked = v.leak();
assert!(leaked.len() == 3);
unsafe {
drop(crate::boxed::Box::from_raw(leaked as *mut [i32]));
}
Comment on lines +4409 to 4411
Copy link

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 uses AI. Check for mistakes.
}

// Check that all other unaffected elements remain unchanged
let k = kani::any_where(|&x: &usize| x < original_len - 1);
if k != index {
assert!(vect[k] == arr[k]);
#[kani::proof]
pub fn verify_spare_capacity_mut() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.reserve(2);
assert!(v.spare_capacity_mut().len() >= 2);
}

#[kani::proof]
pub fn verify_split_at_spare_mut() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.reserve(2);
let (init, spare) = v.split_at_spare_mut();
assert!(init.len() == ARRAY_LEN);
assert!(spare.len() >= 2);
}

#[kani::proof]
pub fn verify_into_boxed_slice() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let v = Vec::from(&arr);
let b = v.into_boxed_slice();
assert!(b.len() == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_into_raw_parts_with_alloc() {
let v = Vec::from(&[1i32, 2, 3]);
let (ptr, len, cap, _alloc) = v.into_raw_parts_with_alloc();
assert!(len == 3);
unsafe {
drop(Vec::from_raw_parts(ptr, len, cap));
}
}

#[kani::proof]
pub fn verify_append() {
let mut v1 = Vec::from(&[1i32, 2]);
let mut v2 = Vec::from(&[3i32, 4]);
v1.append(&mut v2);
assert!(v1.len() == 4);
assert!(v2.is_empty());
}

#[kani::proof]
pub fn verify_split_off() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let at: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
let v2 = v.split_off(at);
assert!(v.len() + v2.len() == ARRAY_LEN);
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_retain_mut() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.retain_mut(|x| *x > 0);
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_dedup_by() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.dedup_by(|a, b| *a == *b);
}

#[kani::proof]
pub fn verify_drain() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let d: Vec<i32> = v.drain(..).collect();
assert!(v.is_empty());
assert!(d.len() == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_into_iter() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let v = Vec::from(&arr);
let c: Vec<i32> = v.into_iter().collect();
assert!(c.len() == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_extend_from_within() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.extend_from_within(..);
assert!(v.len() == ARRAY_LEN * 2);
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_extend_with() {
let mut v: Vec<i32> = Vec::new();
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
v.extend_with(n, 42);
assert!(v.len() == n);
}

#[kani::proof]
pub fn verify_into_flattened() {
let inner: [[i32; 2]; 2] = kani::Arbitrary::any_array();
let v = Vec::from(&inner);
let flat = v.into_flattened();
assert!(flat.len() == 4);
}

#[kani::proof]
pub fn verify_from_raw_parts() {
let mut v = Vec::from(&[1i32, 2, 3]);
let (ptr, len, cap) = (v.as_mut_ptr(), v.len(), v.capacity());
core::mem::forget(v);
let r = unsafe { Vec::from_raw_parts(ptr, len, cap) };
assert!(r.len() == 3);
}

#[kani::proof]
pub fn verify_from_nonnull() {
let mut v = Vec::from(&[1i32, 2, 3]);
let (ptr, len, cap) =
(unsafe { core::ptr::NonNull::new_unchecked(v.as_mut_ptr()) }, v.len(), v.capacity());
core::mem::forget(v);
let r = unsafe { Vec::from_parts(ptr, len, cap) };
assert!(r.len() == 3);
}

#[kani::proof]
pub fn verify_from_nonnull_in() {
let mut v = Vec::from(&[1i32, 2, 3]);
let len = v.len();
let cap = v.capacity();
let ptr = unsafe { core::ptr::NonNull::new_unchecked(v.as_mut_ptr()) };
let alloc = v.allocator().clone();
core::mem::forget(v);
let r = unsafe { Vec::from_parts_in(ptr, len, cap, alloc) };
assert!(r.len() == 3);
}

#[kani::proof]
pub fn verify_set_len() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
unsafe {
v.set_len(n);
}
assert!(v.len() == n);
}

#[kani::proof]
pub fn verify_append_elements() {
let mut v = Vec::from(&[1i32, 2]);
let other = [3i32, 4];
unsafe {
v.append_elements(&other as *const [i32]);
}
assert!(v.len() == 4);
}

#[kani::proof]
pub fn verify_split_at_spare_mut_with_len() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.reserve(2);
let (init, spare, len_ref) = unsafe { v.split_at_spare_mut_with_len() };
assert!(init.len() == ARRAY_LEN);
assert!(spare.len() >= 2);
assert!(*len_ref == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_spec_extend_from_within() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
v.extend_from_within(0..v.len());
assert!(v.len() == ARRAY_LEN * 2);
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_extract_if() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let e: Vec<i32> = v.extract_if(.., |x| *x > 0).collect();
assert!(v.len() + e.len() == ARRAY_LEN);
}

#[kani::proof]
pub fn verify_drop() {
let v = Vec::from(&[1i32, 2, 3]);
drop(v);
}

#[kani::proof]
pub fn verify_try_from() {
let v = Vec::from(&[1i32, 2, 3]);
let r: Result<crate::boxed::Box<[i32; 3]>, _> = v.try_into();
assert!(r.is_ok());
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_extend_desugared() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let extra: [i32; 2] = kani::Arbitrary::any_array();
v.extend_desugared(extra.into_iter());
assert!(v.len() == ARRAY_LEN + 2);
}

#[kani::proof]
#[kani::unwind(4)]
pub fn verify_extend_trusted() {
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
let mut v = Vec::from(&arr);
let extra: [i32; 2] = kani::Arbitrary::any_array();
v.extend_trusted(extra.into_iter());
assert!(v.len() == ARRAY_LEN + 2);
}
}
Loading