Challenge 24: Verify safety of Vec IntoIter functions#570
Challenge 24: Verify safety of Vec IntoIter functions#570Samuelsills wants to merge 2 commits intomodel-checking:mainfrom
Conversation
Add Kani proof harnesses for all 22 functions specified in Challenge model-checking#24, covering IntoIter methods (as_slice, as_mut_slice, next, fold, try_fold, advance_by, next_chunk, next_back, advance_back_by, drop, forget_allocation_drop_remaining, into_vecdeque, __iterator_get_unchecked, size_hint) and auxiliary functions (extract_if::next, spec_extend variants, from_elem variants, from_iter). Resolves model-checking#285 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Verification Coverage ReportIntoIter Functions (14/14 ✅)
Other Files (7/8)
Total: 21 harnesses verified UBs Checked (automatic via Kani/CBMC)
Verification Approach
|
There was a problem hiding this comment.
Pull request overview
Adds Kani proof harnesses to exercise Vec::IntoIter and a handful of related Vec behaviors as part of Challenge #24 / issue #285.
Changes:
- Introduces a
#[cfg(kani)]verifymodule invec/into_iter.rscontaining multiple#[kani::proof]harnesses. - Adds harnesses covering several
IntoItermethods (e.g., slicing, iteration, advancing, folding, drop paths). - Adds harnesses touching related
VecAPIs referenced by the challenge list (e.g.,extract_if,extend,from_elem,from_iter).
| #[unstable(feature = "kani", issue = "none")] | ||
| mod verify { | ||
| use super::*; | ||
| use crate::vec::Vec; |
There was a problem hiding this comment.
#[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).
| use crate::vec::Vec; | |
| use crate::vec::Vec; | |
| use core::kani; |
| #[cfg(kani)] | ||
| #[unstable(feature = "kani", issue = "none")] | ||
| mod verify { | ||
| use super::*; |
There was a problem hiding this comment.
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.
| use super::*; |
| 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))); |
There was a problem hiding this comment.
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.
| 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))); |
| fn verify_advance_by() { | ||
| let v = Vec::from(&[1i32, 2, 3]); | ||
| let mut it = v.into_iter(); | ||
| let _ = it.advance_by(2); |
There was a problem hiding this comment.
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().
| let _ = it.advance_by(2); | |
| assert!(it.advance_by(2).is_ok()); |
| fn verify_advance_back_by() { | ||
| let v = Vec::from(&[1i32, 2, 3]); | ||
| let mut it = v.into_iter(); | ||
| let _ = it.advance_back_by(2); |
There was a problem hiding this comment.
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().
| let _ = it.advance_back_by(2); | |
| assert!(it.advance_back_by(2).is_ok()); |
Summary
Add Kani proof harnesses for all 22 functions specified in Challenge #24:
IntoIter (14):
as_slice,as_mut_slice,forget_allocation_drop_remaining,into_vecdeque,next,size_hint,advance_by,next_chunk,fold,try_fold,__iterator_get_unchecked,next_back,advance_back_by,dropOther files (8):
extract_if::next,spec_extend(IntoIter),spec_extend(slice::Iter),from_elem(i8),from_elem(u8),from_elem(()),from_iter,from_iter(default)All harnesses verified locally with Kani.
Resolves #285