Skip to content

Challenge 24: Verify safety of Vec IntoIter functions #570

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 2 commits into
base: main
Choose a base branch
from
Open

Challenge 24: Verify safety of Vec IntoIter functions #570

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a191053
Challenge 24: Verify safety of Vec IntoIter functions part 2
Samuelsills Mar 26, 2026
6f76315
Fix formatting to match CI rustfmt expectations
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
162 changes: 162 additions & 0 deletions library/alloc/src/vec/into_iter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -541,3 +541,165 @@ unsafe impl<T> AsVecIntoIter for IntoIter<T> {
self
}
}

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
use super::*;
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.

use super::*; appears unused within this verify module (all uses are via inherent methods and Vec from crate::vec::Vec). In the standard library build, unused imports are typically treated as warnings/errors, so consider removing the glob import or importing only the specific items you actually reference by name.

Suggested change
use super::*;

Copilot uses AI. Check for mistakes.
use crate::vec::Vec;
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.

#[kani::proof] / #[kani::unwind] attributes inside this verify module require a kani path in this module’s scope (other #[cfg(kani)] verify modules do use core::kani;). As written, this module doesn’t import core::kani, so it likely won’t compile under cfg(kani) unless there is an external crate named kani in the extern prelude. Add use core::kani; inside the module (or qualify the attributes appropriately).

Suggested change
use crate::vec::Vec;
use crate::vec::Vec;
use core::kani;

Copilot uses AI. Check for mistakes.

const N: usize = 3;

#[kani::proof]
fn verify_as_slice() {
let v = Vec::from(&[1i32, 2, 3]);
let it = v.into_iter();
assert!(it.as_slice().len() == N);
}

#[kani::proof]
fn verify_as_mut_slice() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
it.as_mut_slice()[0] = 42;
}

#[kani::proof]
fn verify_next() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
assert!(it.next() == Some(1));
}

#[kani::proof]
fn verify_size_hint() {
let v = Vec::from(&[1i32, 2, 3]);
let it = v.into_iter();
assert!(it.size_hint() == (N, Some(N)));
Comment on lines +555 to +578
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.

These Kani harnesses use only fixed, concrete inputs (e.g., Vec::from(&[1,2,3])), which proves behavior only for that single case and won’t exercise important edge cases (empty vec, partial consumption, ZSTs, OOM paths, etc.). Other Kani proofs in this repository use nondeterministic values (e.g., kani::Arbitrary::any_array() + kani::any_where(...); see library/alloc/src/vec/mod.rs’s verify module) to get meaningful safety coverage. Consider switching these harnesses to use kani::Arbitrary/kani::any_* inputs with appropriate assumptions to better match the PR’s stated goal of verifying safety of these APIs.

Suggested change
let v = Vec::from(&[1i32, 2, 3]);
let it = v.into_iter();
assert!(it.as_slice().len() == N);
}
#[kani::proof]
fn verify_as_mut_slice() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
it.as_mut_slice()[0] = 42;
}
#[kani::proof]
fn verify_next() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
assert!(it.next() == Some(1));
}
#[kani::proof]
fn verify_size_hint() {
let v = Vec::from(&[1i32, 2, 3]);
let it = v.into_iter();
assert!(it.size_hint() == (N, Some(N)));
// Use arbitrary elements and an arbitrary length up to N
let data: [i32; N] = kani::Arbitrary::any_array();
let len: usize = kani::any();
kani::assume(len <= N);
let mut v = Vec::with_capacity(N);
for i in 0..len {
v.push(data[i]);
}
let it = v.into_iter();
let slice = it.as_slice();
assert!(slice.len() == len);
}
#[kani::proof]
fn verify_as_mut_slice() {
// Use arbitrary elements and an arbitrary length up to N
let data: [i32; N] = kani::Arbitrary::any_array();
let len: usize = kani::any();
kani::assume(len <= N);
let mut v = Vec::with_capacity(N);
for i in 0..len {
v.push(data[i]);
}
let mut it = v.into_iter();
if len > 0 {
it.as_mut_slice()[0] = 42;
}
}
#[kani::proof]
fn verify_next() {
// Require at least one element so that next() returns Some(_)
let data: [i32; N] = kani::Arbitrary::any_array();
let len: usize = kani::any();
kani::assume(len <= N && len > 0);
let first = data[0];
let mut v = Vec::with_capacity(N);
for i in 0..len {
v.push(data[i]);
}
let mut it = v.into_iter();
assert!(it.next() == Some(first));
}
#[kani::proof]
fn verify_size_hint() {
// For a fresh IntoIter, size_hint should match the remaining length
let data: [i32; N] = kani::Arbitrary::any_array();
let len: usize = kani::any();
kani::assume(len <= N);
let mut v = Vec::with_capacity(N);
for i in 0..len {
v.push(data[i]);
}
let it = v.into_iter();
assert!(it.size_hint() == (len, Some(len)));

Copilot uses AI. Check for mistakes.
}

#[kani::proof]
fn verify_advance_by() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
let _ = it.advance_by(2);
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.

advance_by returns a Result indicating whether the requested number of steps was fully advanced. Currently the result is ignored, so the harness won’t fail if advance_by(2) unexpectedly returns Err(_). Consider asserting it.advance_by(2).is_ok() (or unwrap()), then checking the postcondition on len().

Suggested change
let _ = it.advance_by(2);
assert!(it.advance_by(2).is_ok());

Copilot uses AI. Check for mistakes.
assert!(it.len() == 1);
}

#[kani::proof]
fn verify_next_chunk() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
let chunk = it.next_chunk::<2>();
assert!(chunk.is_ok());
}

#[kani::proof]
#[kani::unwind(4)]
fn verify_fold() {
let v = Vec::from(&[1i32, 2, 3]);
let sum = v.into_iter().fold(0i32, |a, x| a + x);
assert!(sum == 6);
}

#[kani::proof]
#[kani::unwind(4)]
fn verify_try_fold() {
let v = Vec::from(&[1i32, 2, 3]);
let r: Result<i32, ()> = v.into_iter().try_fold(0, |a, x| Ok(a + x));
assert!(r == Ok(6));
}

#[kani::proof]
fn verify_iterator_get_unchecked() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
let val = unsafe { it.__iterator_get_unchecked(1) };
assert!(val == 2);
}

#[kani::proof]
fn verify_next_back() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
assert!(it.next_back() == Some(3));
}

#[kani::proof]
fn verify_advance_back_by() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
let _ = it.advance_back_by(2);
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.

advance_back_by returns a Result indicating whether the requested number of steps was fully advanced. The harness ignores it, so it wouldn’t catch an unexpected Err(_). Consider asserting the return value is Ok(()) (or unwrapping) before checking len().

Suggested change
let _ = it.advance_back_by(2);
assert!(it.advance_back_by(2).is_ok());

Copilot uses AI. Check for mistakes.
assert!(it.len() == 1);
}

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

#[kani::proof]
fn verify_forget_allocation_drop_remaining() {
let v = Vec::from(&[1i32, 2, 3]);
let mut it = v.into_iter();
it.next();
it.forget_allocation_drop_remaining();
}

#[kani::proof]
fn verify_into_vecdeque() {
let v = Vec::from(&[1i32, 2, 3]);
let d = v.into_iter().into_vecdeque();
assert!(d.len() == N);
}

#[kani::proof]
#[kani::unwind(4)]
fn verify_extract_if_next() {
let mut v = Vec::from(&[1i32, 2, 3]);
let e: Vec<i32> = v.extract_if(.., |x| *x > 1).collect();
assert!(v.len() + e.len() == N);
}

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

#[kani::proof]
#[kani::unwind(4)]
fn verify_spec_extend_slice_iter() {
let mut v = Vec::from(&[1i32, 2]);
v.extend([3i32, 4].iter());
assert!(v.len() == 4);
}

#[kani::proof]
fn verify_from_elem_i8() {
let v: Vec<i8> = crate::vec![42i8; 3];
assert!(v.len() == 3 && v[0] == 42);
}

#[kani::proof]
fn verify_from_elem_u8() {
let v: Vec<u8> = crate::vec![7u8; 3];
assert!(v.len() == 3 && v[0] == 7);
}

#[kani::proof]
fn verify_from_elem_unit() {
let v: Vec<()> = crate::vec![(); 3];
assert!(v.len() == 3);
}

#[kani::proof]
fn verify_from_iter() {
let v: Vec<i32> = [1i32, 2, 3].iter().copied().collect();
assert!(v.len() == 3);
}
}
Loading