Commit 9f4b427
Verify safety of slice iterator functions with Kani (Challenge 18)
52 Kani proof harnesses covering iterator types across
library/core/src/slice/iter.rs and iter/macros.rs:
## Iter (existing 18 harnesses, extended)
- new, clone, count, default, as_slice, as_ref
- next, next_back, nth, nth_back, advance_by, advance_back_by
- is_empty, len, size_hint
- post_inc_start, pre_dec_end, next_back_unchecked (unsafe)
- Verified with: (), u8, char, (char, u8)
## IterMut (5 new harnesses)
- new, into_slice, as_mut_slice, next, next_back
## Split (2 new harnesses)
- next, next_back (with concrete predicate)
## Chunks (3 new harnesses)
- next, next_back, __iterator_get_unchecked
## ChunksMut (4 new harnesses)
- next, nth, next_back, nth_back
## ChunksExact / ChunksExactMut (5 new harnesses)
- new (ChunksExact), next/nth/next_back/nth_back (ChunksExactMut)
## RChunks / RChunksMut (7 new harnesses)
- next, next_back (RChunks)
- next, nth, last, next_back, nth_back (RChunksMut)
## RChunksExact / RChunksExactMut (5 new harnesses)
- new (RChunksExact)
- next, nth, next_back, nth_back (RChunksExactMut)
## ArrayWindows (5 new harnesses, const generic)
- next/next_back (N=1,2,4), nth/nth_back (N=2,4)
## Windows (1 new harness)
- __iterator_get_unchecked
## __iterator_get_unchecked (6 new harnesses)
- ChunksMut, ChunksExact, RChunks, RChunksMut, RChunksExact, RChunksExactMut
## Macro functions: fold, for_each, position, rposition (7 new harnesses)
- Iter: fold, for_each, position, rposition
- IterMut: fold, for_each, position
Resolves #282
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>1 parent 7af3f89 commit 9f4b427
1 file changed
+578
-0
lines changed
0 commit comments