Challenge 18: Verify safety of Slice iterator functions by Samuelsills · Pull Request #568 · model-checking/verify-rust-std

Samuelsills · 2026-03-26T14:01:02Z

Summary

Add Kani proof harnesses verifying slice iterator functions specified in Challenge #18:

Safe abstractions for Iter/IterMut: new, into_slice, as_mut_slice, last, fold, for_each, position, rposition
Safe abstractions for Split: next, next_back
Safe abstractions for chunk iterators: next, nth, next_back, nth_back, new, last across Chunks, ChunksMut, ChunksExact, ChunksExactMut, ArrayWindows, RChunks, RChunksMut, RChunksExact, RChunksExactMut
Unsafe __iterator_get_unchecked: Windows, Chunks, ChunksMut, ChunksExact, ChunksExactMut, RChunks, RChunksMut, RChunksExact, RChunksExactMut

Builds on pre-existing Iter harnesses (Part 1 macro functions) which cover make_slice, len, is_empty, next, size_hint, count, nth, advance_by, next_back, nth_back, advance_back_by.

All harnesses verified locally with Kani.

Resolves #282

Add Kani proof harnesses for slice iterator functions specified in Challenge model-checking#18, covering safe abstractions and unsafe __iterator_get_unchecked implementations for Chunks, ChunksMut, ChunksExact, ChunksExactMut, Windows, ArrayWindows, RChunks, RChunksMut, RChunksExact, RChunksExactMut, Split, Iter, and IterMut. Resolves model-checking#282 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Samuelsills · 2026-03-29T16:01:23Z

Verification Coverage Report

Part 1: Macro Functions (16/16 ✅)

Pre-existing harnesses verify make_slice, len, is_empty, next, size_hint, count, nth, advance_by, last, fold, for_each, position, rposition, next_back, nth_back, advance_back_by across multiple types (u8, char, (), (char, u8)).

Part 2: Unsafe `__iterator_get_unchecked` (9/12)

Windows, Chunks, ChunksMut, ChunksExact, ChunksExactMut, RChunks, RChunksMut, RChunksExact, RChunksExactMut — all verified.

Part 2: Safe Abstractions (39/39 ✅)

All chunk iterator next, nth, next_back, nth_back, new, last methods verified across Chunks, ChunksMut, ChunksExact, ChunksExactMut, ArrayWindows, RChunks, RChunksMut, RChunksExact, RChunksExactMut, Split, Iter, IterMut.

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
Builds on pre-existing Iter/IterMut harnesses (Part 1)
50+ new harnesses for Part 2 chunk/window/split iterators

Copilot

Pull request overview

Adds additional Kani proof harnesses under #[cfg(kani)] to exercise (and locally verify) safety-related behavior for various slice iterator adapters and their hidden __iterator_get_unchecked implementations as part of Challenge #18 / issue #282.

Changes:

Added new Kani proofs for Iter / IterMut-related iterator operations (last, fold, for_each, position, rposition, into_slice, as_mut_slice).
Added new Kani proofs for Split, chunk-based iterators, array_windows, and reverse chunk iterators (next, nth, next_back, nth_back, last, and constructors/remainders in a few cases).
Added Kani proofs calling unsafe __iterator_get_unchecked for multiple slice iterator adapter types with bounded indices.

Copilot · 2026-03-31T22:24:18Z

library/core/src/slice/iter.rs

+        let arr: [i32; 5] = kani::any();
+        let s: &[i32] = &arr;
+        let iter = s.iter();
+        let last = iter.last();
+        assert_eq!(*last.unwrap(), arr[4]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn verify_iter_fold() {
+        let arr: [i32; 3] = kani::any();
+        let s: &[i32] = &arr;
+        let sum = s.iter().fold(0i32, |acc, &x| acc.wrapping_add(x));
+        assert_eq!(sum, arr[0].wrapping_add(arr[1]).wrapping_add(arr[2]));


These Kani proofs use fixed-size arrays (e.g., [i32; 5]) and then assert specific functional results. That only verifies the behavior for that exact length and doesn't exercise the any_slice/any_iter pattern used elsewhere in this verify module to cover arbitrary (including empty) slices and pointer/len edge cases relevant to safety. Consider rewriting these harnesses to build the iterator from any_slice/any_iter (and avoid unwrap() unless you kani::assume non-empty) so the proofs actually target the safety/invariant surface across lengths rather than a single concrete case.

Suggested change

let arr: [i32; 5] = kani::any();

let s: &[i32] = &arr;

let iter = s.iter();

let last = iter.last();

assert_eq!(*last.unwrap(), arr[4]);

}

#[kani::proof]

#[kani::unwind(6)]

fn verify_iter_fold() {

let arr: [i32; 3] = kani::any();

let s: &[i32] = &arr;

let sum = s.iter().fold(0i32, |acc, &x| acc.wrapping_add(x));

assert_eq!(sum, arr[0].wrapping_add(arr[1]).wrapping_add(arr[2]));

let s: &[i32] = kani::any_slice();

let iter = s.iter();

let last = iter.last();

match last {

Some(&value) => {

let len = s.len();

// If `last` returns Some, the slice must be non-empty,

// and the value must equal the last element.

assert!(len > 0);

assert_eq!(value, s[len - 1]);

}

None => {

// If `last` returns None, the slice must be empty.

assert!(s.is_empty());

}

}

}

#[kani::proof]

#[kani::unwind(6)]

fn verify_iter_fold() {

let s: &[i32] = kani::any_slice();

let sum = s.iter().fold(0i32, |acc, &x| acc.wrapping_add(x));

// Compute the expected result with an explicit loop to

// cross-check `fold` for arbitrary slice lengths.

let mut expected = 0i32;

for &x in s {

expected = expected.wrapping_add(x);

}

assert_eq!(sum, expected);

Copilot · 2026-03-31T22:24:19Z

library/core/src/slice/iter.rs

+    #[kani::proof]
+    fn verify_iter_mut_new() {
+        let mut arr: [i32; 5] = kani::any();
+        let s: &mut [i32] = &mut arr;
+        let iter = s.iter_mut();
+        assert_eq!(iter.len(), 5);
+    }


verify_iter_mut_new is described as covering the safe abstraction IterMut::new, but it only calls slice.iter_mut() and checks len(). If the goal is to verify IterMut::new specifically (and the iterator safety invariant), consider constructing with IterMut::new(&mut ...) here and asserting iter.is_safe() (as done for Iter in check_new_iter).

Copilot · 2026-03-31T22:24:19Z

library/core/src/slice/iter.rs

+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn verify_iter_position() {
+        let arr: [i32; 5] = kani::any();
+        let s: &[i32] = &arr;
+        let target = arr[2];
+        let pos = s.iter().position(|&x| x == target);
+        assert!(pos.is_some());
+        assert!(pos.unwrap() <= 2);
+    }


Within this #[cfg(kani)] mod verify block, the existing harness generators use kani::assert(...) (e.g., line 3306) rather than assert!/assert_eq!. Using assert! will panic on failure and provides less Kani-specific context; for consistency with the rest of this module, consider switching these new harness assertions to kani::assert / kani::assert_eq-style checks (or add messages).

Copilot · 2026-03-31T22:24:19Z

library/core/src/slice/iter.rs

+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn verify_chunks_next_back() {
+        let arr: [i32; 5] = kani::any();
+        let s: &[i32] = &arr;
+        let mut chunks = s.chunks(2);
+        let last = chunks.next_back();
+        assert!(last.is_some());
+        assert_eq!(last.unwrap().len(), 1);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn verify_chunks_mut_next() {
+        let mut arr: [i32; 5] = kani::any();
+        let s: &mut [i32] = &mut arr;
+        let mut chunks = s.chunks_mut(2);
+        let first = chunks.next();
+        assert!(first.is_some());
+        assert_eq!(first.unwrap().len(), 2);
+    }
+


This section adds many highly repetitive harnesses for chunk iterators that differ only by iterator type/method and a few expected lengths. Since this verify module already uses macros to generate harnesses (e.g., check_iter_with_ty! / check_safe_abstraction!), consider introducing a small macro/helper for these chunk/split/window harnesses as well to reduce duplication and make it easier to audit completeness against the Challenge #18 checklist.

Suggested change

#[kani::proof]

#[kani::unwind(6)]

fn verify_chunks_next_back() {

let arr: [i32; 5] = kani::any();

let s: &[i32] = &arr;

let mut chunks = s.chunks(2);

let last = chunks.next_back();

assert!(last.is_some());

assert_eq!(last.unwrap().len(), 1);

}

#[kani::proof]

#[kani::unwind(6)]

fn verify_chunks_mut_next() {

let mut arr: [i32; 5] = kani::any();

let s: &mut [i32] = &mut arr;

let mut chunks = s.chunks_mut(2);

let first = chunks.next();

assert!(first.is_some());

assert_eq!(first.unwrap().len(), 2);

}

#[cfg(kani)]

macro_rules! kani_chunks_harness_immut {

($name:ident, $iter_method:ident, $next_method:ident, $expected_len:expr) => {

#[kani::proof]

#[kani::unwind(6)]

fn $name() {

let arr: [i32; 5] = kani::any();

let s: &[i32] = &arr;

let mut iter = s.$iter_method(2);

let item = iter.$next_method();

assert!(item.is_some());

assert_eq!(item.unwrap().len(), $expected_len);

}

};

}

#[cfg(kani)]

macro_rules! kani_chunks_harness_mut {

($name:ident, $iter_method:ident, $next_method:ident, $expected_len:expr) => {

#[kani::proof]

#[kani::unwind(6)]

fn $name() {

let mut arr: [i32; 5] = kani::any();

let s: &mut [i32] = &mut arr;

let mut iter = s.$iter_method(2);

let item = iter.$next_method();

assert!(item.is_some());

assert_eq!(item.unwrap().len(), $expected_len);

}

};

}

kani_chunks_harness_immut!(verify_chunks_next_back, chunks, next_back, 1);

kani_chunks_harness_mut!(verify_chunks_mut_next, chunks_mut, next, 2);

Samuelsills marked this pull request as ready for review March 26, 2026 20:25

Samuelsills requested a review from a team as a code owner March 26, 2026 20:25

feliperodri added the Challenge Used to tag a challenge label Mar 29, 2026

feliperodri requested a review from Copilot March 31, 2026 22:18

Copilot started reviewing on behalf of feliperodri March 31, 2026 22:19 View session

Copilot AI reviewed Mar 31, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Challenge 18: Verify safety of Slice iterator functions#568

Challenge 18: Verify safety of Slice iterator functions#568
Samuelsills wants to merge 1 commit intomodel-checking:mainfrom
Samuelsills:challenge-18-slice-iter

Samuelsills commented Mar 26, 2026

Uh oh!

Samuelsills commented Mar 29, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Samuelsills commented Mar 26, 2026

Summary

Uh oh!

Samuelsills commented Mar 29, 2026

Verification Coverage Report

Part 1: Macro Functions (16/16 ✅)

Part 2: Unsafe __iterator_get_unchecked (9/12)

Part 2: Safe Abstractions (39/39 ✅)

UBs Checked (automatic via Kani/CBMC)

Verification Approach

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 31, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Part 2: Unsafe `__iterator_get_unchecked` (9/12)