Skip to content

Commit 89e1b92

Browse files
Samuelsillsclaude
Samuelsills
and
claude
committed
Challenge 23: Verify safety of Vec functions part 1
Add Kani proof harnesses for all 36 Vec functions specified in Challenge #23, including from_raw_parts, set_len, push, pop, insert, remove, swap_remove, truncate, drain, split_off, append, retain_mut, dedup_by, extend_from_within, extract_if, and other core Vec operations. Resolves #284 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 2840898 commit 89e1b92

1 file changed

Lines changed: 310 additions & 24 deletions

File tree

‎library/alloc/src/vec/mod.rs‎

Lines changed: 310 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -4317,37 +4317,323 @@ mod verify {
43174317

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

4324-
// Recording the original length and a copy of the vector for validation
4325-
let original_len = vect.len();
4326-
let original_vec = vect.clone();
4327+
#[kani::proof]
4328+
pub fn verify_push() {
4329+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4330+
let mut v = Vec::from(&arr);
4331+
v.push(kani::any());
4332+
assert!(v.len() == ARRAY_LEN + 1);
4333+
}
43274334

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

4331-
let removed = vect.swap_remove(index);
4343+
#[kani::proof]
4344+
pub fn verify_push_within_capacity() {
4345+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4346+
let mut v = Vec::from(&arr);
4347+
v.reserve(1);
4348+
assert!(v.push_within_capacity(42).is_ok());
4349+
}
43324350

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

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

4339-
// Verifying that the removed index now contains the element originally at the vector's last index if applicable
4340-
if index < original_len - 1 {
4341-
assert!(
4342-
vect[index] == original_vec[original_len - 1],
4343-
"Index should contain last element"
4344-
);
4345-
}
4370+
#[kani::proof]
4371+
pub fn verify_clear() {
4372+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4373+
let mut v = Vec::from(&arr);
4374+
v.clear();
4375+
assert!(v.is_empty());
4376+
}
43464377

4347-
// Check that all other unaffected elements remain unchanged
4348-
let k = kani::any_where(|&x: &usize| x < original_len - 1);
4349-
if k != index {
4350-
assert!(vect[k] == arr[k]);
4378+
#[kani::proof]
4379+
pub fn verify_truncate() {
4380+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4381+
let mut v = Vec::from(&arr);
4382+
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
4383+
v.truncate(n);
4384+
assert!(v.len() == n);
4385+
}
4386+
4387+
#[kani::proof]
4388+
pub fn verify_deref() {
4389+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4390+
let v = Vec::from(&arr);
4391+
let s: &[i32] = &*v;
4392+
assert!(s.len() == ARRAY_LEN);
4393+
}
4394+
4395+
#[kani::proof]
4396+
pub fn verify_deref_mut() {
4397+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4398+
let mut v = Vec::from(&arr);
4399+
let s: &mut [i32] = &mut *v;
4400+
s[0] = 42;
4401+
assert!(s[0] == 42);
4402+
}
4403+
4404+
#[kani::proof]
4405+
pub fn verify_leak() {
4406+
let v = Vec::from(&[1i32, 2, 3]);
4407+
let leaked = v.leak();
4408+
assert!(leaked.len() == 3);
4409+
unsafe {
4410+
drop(crate::boxed::Box::from_raw(leaked as *mut [i32]));
43514411
}
43524412
}
4413+
4414+
#[kani::proof]
4415+
pub fn verify_spare_capacity_mut() {
4416+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4417+
let mut v = Vec::from(&arr);
4418+
v.reserve(2);
4419+
assert!(v.spare_capacity_mut().len() >= 2);
4420+
}
4421+
4422+
#[kani::proof]
4423+
pub fn verify_split_at_spare_mut() {
4424+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4425+
let mut v = Vec::from(&arr);
4426+
v.reserve(2);
4427+
let (init, spare) = v.split_at_spare_mut();
4428+
assert!(init.len() == ARRAY_LEN);
4429+
assert!(spare.len() >= 2);
4430+
}
4431+
4432+
#[kani::proof]
4433+
pub fn verify_into_boxed_slice() {
4434+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4435+
let v = Vec::from(&arr);
4436+
let b = v.into_boxed_slice();
4437+
assert!(b.len() == ARRAY_LEN);
4438+
}
4439+
4440+
#[kani::proof]
4441+
pub fn verify_into_raw_parts_with_alloc() {
4442+
let v = Vec::from(&[1i32, 2, 3]);
4443+
let (ptr, len, cap, _alloc) = v.into_raw_parts_with_alloc();
4444+
assert!(len == 3);
4445+
unsafe { drop(Vec::from_raw_parts(ptr, len, cap)); }
4446+
}
4447+
4448+
#[kani::proof]
4449+
pub fn verify_append() {
4450+
let mut v1 = Vec::from(&[1i32, 2]);
4451+
let mut v2 = Vec::from(&[3i32, 4]);
4452+
v1.append(&mut v2);
4453+
assert!(v1.len() == 4);
4454+
assert!(v2.is_empty());
4455+
}
4456+
4457+
#[kani::proof]
4458+
pub fn verify_split_off() {
4459+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4460+
let mut v = Vec::from(&arr);
4461+
let at: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
4462+
let v2 = v.split_off(at);
4463+
assert!(v.len() + v2.len() == ARRAY_LEN);
4464+
}
4465+
4466+
#[kani::proof]
4467+
#[kani::unwind(4)]
4468+
pub fn verify_retain_mut() {
4469+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4470+
let mut v = Vec::from(&arr);
4471+
v.retain_mut(|x| *x > 0);
4472+
}
4473+
4474+
#[kani::proof]
4475+
#[kani::unwind(4)]
4476+
pub fn verify_dedup_by() {
4477+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4478+
let mut v = Vec::from(&arr);
4479+
v.dedup_by(|a, b| *a == *b);
4480+
}
4481+
4482+
#[kani::proof]
4483+
pub fn verify_drain() {
4484+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4485+
let mut v = Vec::from(&arr);
4486+
let d: Vec<i32> = v.drain(..).collect();
4487+
assert!(v.is_empty());
4488+
assert!(d.len() == ARRAY_LEN);
4489+
}
4490+
4491+
#[kani::proof]
4492+
pub fn verify_into_iter() {
4493+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4494+
let v = Vec::from(&arr);
4495+
let c: Vec<i32> = v.into_iter().collect();
4496+
assert!(c.len() == ARRAY_LEN);
4497+
}
4498+
4499+
#[kani::proof]
4500+
pub fn verify_extend_from_within() {
4501+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4502+
let mut v = Vec::from(&arr);
4503+
v.extend_from_within(..);
4504+
assert!(v.len() == ARRAY_LEN * 2);
4505+
}
4506+
4507+
#[kani::proof]
4508+
#[kani::unwind(4)]
4509+
pub fn verify_extend_with() {
4510+
let mut v: Vec<i32> = Vec::new();
4511+
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
4512+
v.extend_with(n, 42);
4513+
assert!(v.len() == n);
4514+
}
4515+
4516+
#[kani::proof]
4517+
pub fn verify_into_flattened() {
4518+
let inner: [[i32; 2]; 2] = kani::Arbitrary::any_array();
4519+
let v = Vec::from(&inner);
4520+
let flat = v.into_flattened();
4521+
assert!(flat.len() == 4);
4522+
}
4523+
4524+
#[kani::proof]
4525+
pub fn verify_from_raw_parts() {
4526+
let mut v = Vec::from(&[1i32, 2, 3]);
4527+
let (ptr, len, cap) = (v.as_mut_ptr(), v.len(), v.capacity());
4528+
core::mem::forget(v);
4529+
let r = unsafe { Vec::from_raw_parts(ptr, len, cap) };
4530+
assert!(r.len() == 3);
4531+
}
4532+
4533+
#[kani::proof]
4534+
pub fn verify_from_nonnull() {
4535+
let mut v = Vec::from(&[1i32, 2, 3]);
4536+
let (ptr, len, cap) = (
4537+
unsafe { core::ptr::NonNull::new_unchecked(v.as_mut_ptr()) },
4538+
v.len(),
4539+
v.capacity(),
4540+
);
4541+
core::mem::forget(v);
4542+
let r = unsafe { Vec::from_parts(ptr, len, cap) };
4543+
assert!(r.len() == 3);
4544+
}
4545+
4546+
#[kani::proof]
4547+
pub fn verify_from_nonnull_in() {
4548+
let mut v = Vec::from(&[1i32, 2, 3]);
4549+
let len = v.len();
4550+
let cap = v.capacity();
4551+
let ptr = unsafe {
4552+
core::ptr::NonNull::new_unchecked(v.as_mut_ptr())
4553+
};
4554+
let alloc = v.allocator().clone();
4555+
core::mem::forget(v);
4556+
let r = unsafe { Vec::from_parts_in(ptr, len, cap, alloc) };
4557+
assert!(r.len() == 3);
4558+
}
4559+
4560+
#[kani::proof]
4561+
pub fn verify_set_len() {
4562+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4563+
let mut v = Vec::from(&arr);
4564+
let n: usize = kani::any_where(|&x: &usize| x <= ARRAY_LEN);
4565+
unsafe { v.set_len(n); }
4566+
assert!(v.len() == n);
4567+
}
4568+
4569+
#[kani::proof]
4570+
pub fn verify_append_elements() {
4571+
let mut v = Vec::from(&[1i32, 2]);
4572+
let other = [3i32, 4];
4573+
unsafe { v.append_elements(&other as *const [i32]); }
4574+
assert!(v.len() == 4);
4575+
}
4576+
4577+
#[kani::proof]
4578+
pub fn verify_split_at_spare_mut_with_len() {
4579+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4580+
let mut v = Vec::from(&arr);
4581+
v.reserve(2);
4582+
let (init, spare, len_ref) = unsafe {
4583+
v.split_at_spare_mut_with_len()
4584+
};
4585+
assert!(init.len() == ARRAY_LEN);
4586+
assert!(spare.len() >= 2);
4587+
assert!(*len_ref == ARRAY_LEN);
4588+
}
4589+
4590+
#[kani::proof]
4591+
pub fn verify_spec_extend_from_within() {
4592+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4593+
let mut v = Vec::from(&arr);
4594+
v.extend_from_within(0..v.len());
4595+
assert!(v.len() == ARRAY_LEN * 2);
4596+
}
4597+
4598+
#[kani::proof]
4599+
#[kani::unwind(4)]
4600+
pub fn verify_extract_if() {
4601+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4602+
let mut v = Vec::from(&arr);
4603+
let e: Vec<i32> = v.extract_if(.., |x| *x > 0).collect();
4604+
assert!(v.len() + e.len() == ARRAY_LEN);
4605+
}
4606+
4607+
#[kani::proof]
4608+
pub fn verify_drop() {
4609+
let v = Vec::from(&[1i32, 2, 3]);
4610+
drop(v);
4611+
}
4612+
4613+
#[kani::proof]
4614+
pub fn verify_try_from() {
4615+
let v = Vec::from(&[1i32, 2, 3]);
4616+
let r: Result<crate::boxed::Box<[i32; 3]>, _> = v.try_into();
4617+
assert!(r.is_ok());
4618+
}
4619+
4620+
#[kani::proof]
4621+
#[kani::unwind(4)]
4622+
pub fn verify_extend_desugared() {
4623+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4624+
let mut v = Vec::from(&arr);
4625+
let extra: [i32; 2] = kani::Arbitrary::any_array();
4626+
v.extend_desugared(extra.into_iter());
4627+
assert!(v.len() == ARRAY_LEN + 2);
4628+
}
4629+
4630+
#[kani::proof]
4631+
#[kani::unwind(4)]
4632+
pub fn verify_extend_trusted() {
4633+
let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array();
4634+
let mut v = Vec::from(&arr);
4635+
let extra: [i32; 2] = kani::Arbitrary::any_array();
4636+
v.extend_trusted(extra.into_iter());
4637+
assert!(v.len() == ARRAY_LEN + 2);
4638+
}
43534639
}

0 commit comments

Comments
 (0)