Verify safety of iterator adapter functions (Challenge 16) by kasimte · Pull Request #549 · model-checking/verify-rust-std

kasimte · 2026-02-19T01:43:36Z

Resolves #280 (Challenge 16: Verify the safety of Iterator functions)

74 Kani verification harnesses proving the safety of all 10 unsafe functions and all 17 safe abstractions across 13 iterator adapter files in library/core/src/iter/adapters/. 26 of 27 functions have unbounded verification coverage (array_chunks::fold is bounded due to CI time limits; see Known limitations).

Requirements checklist

Requirement	Status	Notes
All 10 unsafe functions	Done	10 `#[requires]` contracts + 36 harnesses (4 types each)
All 17 safe abstractions	Done	38 harnesses across 8 adapter files
Unbounded (arbitrary-length slices)	26/27	Symbolic arrays, loop contracts, inductive decomposition; `array_chunks::fold` is bounded (see below)
Generic type `T`	Pragmatic	Kani requires concrete types; we use 4 types (`u8`, `()`, `char`, `(char,u8)`) covering all behavioral axes (`size_of`, `align_of`, ZST, validity constraints, padding)
Absence of UB	Done	CBMC checks pointer validity, uninitialized reads, immutable mutation, invalid values automatically
Safety contracts	Done	10 `#[requires(...)]` on inherent impl methods; `kani::assume()` for trait impl methods (proc macro limitation)

Known limitations

array_chunks::fold: Bounded harness (MAX_LEN=8, unwind 9). A source-code loop invariant (i <= inner_len) was implemented and verified locally, but the TrustedRandomAccessNoCoerce-specialized fold path with __iterator_get_unchecked consistently exceeded CI's per-harness timeout under loop contract mode (tested at MAX_LEN 1000, 500, 100, and 10). The unsafe operation — __iterator_get_unchecked(i + local) guarded by inner_len - i >= N — is the same indexed access pattern verified unboundedly via loop contracts in take.rs and zip.rs.
next_back_remainder: Uses Range<u8> instead of slice::Iter because CBMC exhausts resources on the pointer-heavy adapter chain. Exercises the same unwrap_err_unchecked code path.
Generic type T: The challenge requires verification without monomorphization. Kani requires concrete types (CBMC operates on concrete GOTO programs), so truly generic proofs are not possible with this tool. The unsafe operations depend on size_of::<T>() and align_of::<T>(), not type identity — our 4 types exhaust these behavioral axes. We defer to the committee's judgment on whether this satisfies the requirement.

Source code modifications

5 loop invariant annotations added via #[cfg_attr(kani, kani::loop_invariant(...))] in take.rs (2) and zip.rs (3). Zero impact on non-Kani builds. 10 safety contracts added via #[requires(...)].

Verification details (click to expand)

Quick verification

./scripts/run-kani.sh --kani-args \
  --harness iter::adapters::copied::verify \
  --harness iter::adapters::cloned::verify \
  --harness iter::adapters::map::verify \
  --harness iter::adapters::enumerate::verify \
  --harness iter::adapters::fuse::verify \
  --harness iter::adapters::skip::verify \
  --harness iter::adapters::zip::verify \
  --harness iter::adapters::array_chunks::verify \
  --harness iter::adapters::filter::verify \
  --harness iter::adapters::filter_map::verify \
  --harness iter::adapters::map_windows::verify \
  --harness iter::adapters::step_by::verify \
  --harness iter::adapters::take::verify \
  --output-format terse

Expected: Complete - 74 successfully verified harnesses, 0 failures, 74 total.

Unbounded verification techniques

Large symbolic arrays — kani::slice::any_slice_of_array with up to 5000 elements (u8), isize::MAX (ZST), 50 (char/tuple). Slice length is fully symbolic within [0, MAX_LEN].
Loop contracts — #[cfg_attr(kani, kani::loop_invariant(...))] on 5 loops in take.rs and zip.rs.
Single-call pattern — For functions where unsafe ops are bounded by a constant (not slice length).
Two-call pattern — MapWindows: 2 calls to next() exercise buffer init + ring buffer wrap.
Inductive decomposition — Unbounded inductive step proves unsafe ops safe at any iteration k, supplemented by bounded end-to-end harnesses. Used for zip::spec_fold, filter::next_chunk_dropless, filter_map::next_chunk.

Safety contracts

Function	File	Contract
`__iterator_get_unchecked`	cloned.rs	`#[requires(idx < self.it.size_hint().0)]`
`next_unchecked`	cloned.rs	`#[requires(self.it.size_hint().0 > 0)]`
`__iterator_get_unchecked`	copied.rs	`#[requires(idx < self.it.size_hint().0)]`
`__iterator_get_unchecked`	enumerate.rs	`#[requires(idx < self.iter.size_hint().0)]`
`__iterator_get_unchecked`	fuse.rs	`#[requires(self.iter.is_some() && idx < self.iter.as_ref().unwrap().size_hint().0)]`
`__iterator_get_unchecked`	map.rs	`#[requires(idx < self.iter.size_hint().0)]`
`next_unchecked`	map.rs	`#[requires(self.iter.size_hint().0 > 0)]`
`__iterator_get_unchecked`	skip.rs	`#[requires(idx + self.n < self.iter.size_hint().0)]`
`__iterator_get_unchecked`	zip.rs	`#[requires(idx < self.size_hint().0)]`
`get_unchecked`	zip.rs	`#[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]`

Unsafe functions (10/10)

Function	File	Harnesses
`__iterator_get_unchecked`	cloned.rs (listed as clone.rs in challenge)	4 (u8, unit, char, tup)
`next_unchecked`	cloned.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	copied.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	enumerate.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	fuse.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	map.rs	4 (u8, unit, char, tup)
`next_unchecked`	map.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	skip.rs	4 (u8, unit, char, tup)
`__iterator_get_unchecked`	zip.rs	4 (u8, unit, char, tup)
`get_unchecked`	zip.rs	same 4 above (called transitively)

Safe abstractions (17/17)

Function	File	Harnesses
`next_back_remainder`	array_chunks.rs	2 (N=2, N=3 via Range<u8>)
`fold`	array_chunks.rs	1 (N=2 u8, bounded e2e)
`spec_next_chunk`	copied.rs	4 (N=2/3 u8, N=2 unit/char)
`next_chunk_dropless`	filter.rs	4 (3 bounded e2e + 1 unbounded inductive)
`next_chunk`	filter_map.rs	4 (3 bounded e2e + 1 unbounded inductive)
`as_array_ref`	map_windows.rs	5 shared (N=2/3 u8, clone N=2, clone-before-next N=2, N=2 char)
`as_uninit_array_mut`	map_windows.rs	same 5 (exercised via Buffer::clone)
`push`	map_windows.rs	same 5 (exercised via iteration)
`drop`	map_windows.rs	same 5 (exercised via iteration)
`original_step`	step_by.rs	4 (size_hint u8/char, next u8, next_back u8)
`spec_fold`	take.rs	4 (u8, unit, char, tup)
`spec_for_each`	take.rs	2 (u8, char)
`fold`	zip.rs	2 (u8, char)
`next`	zip.rs	2 (u8, char)
`nth`	zip.rs	1 (u8)
`next_back`	zip.rs	1 (u8)
`spec_fold`	zip.rs	2 (bounded e2e + unbounded inductive)

Test plan

All 74 harnesses pass locally
CI passes (all partitions green on fork test PR)

Resolves #280

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

74 harnesses proving safety of all 10 unsafe functions and 17 safe abstractions listed in Challenge 16, across 13 iterator adapter files. Unbounded verification via large symbolic arrays, loop contracts, and inductive decomposition. 4 representative types (u8, (), char, (char,u8)) cover all behavioral axes of the generic code.

Copilot

Pull request overview

Adds Kani-based formal verification coverage for iterator adapter implementations in library/core/src/iter/adapters/, including harnesses and contract/invariant annotations to justify the safety of unsafe internals and safe abstractions.

Changes:

Add #[cfg(kani)] verification modules with Kani harnesses across multiple iterator adapters.
Add/extend safety contracts (#[requires(...)]) and Kani loop-invariant annotations (#[cfg_attr(kani, ...)]) to enable (mostly) unbounded verification.
Document verification assumptions/limitations inline (e.g., bounded unwind in some harnesses).

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
library/core/src/iter/adapters/zip.rs	Adds contracts/loop-invariant annotations and extensive Kani harnesses for `Zip` unsafe/specialized paths.
library/core/src/iter/adapters/take.rs	Adds loop-invariant annotations and Kani harnesses for `Take` specialized paths.
library/core/src/iter/adapters/step_by.rs	Adds Kani harnesses exercising `original_step` via multiple entry points.
library/core/src/iter/adapters/skip.rs	Adds Kani harnesses for `Skip::__iterator_get_unchecked`.
library/core/src/iter/adapters/map.rs	Adds Kani harnesses for `Map` unsafe methods.
library/core/src/iter/adapters/map_windows.rs	Adds Kani harnesses targeting buffer initialization/wrap, clone paths, and drop safety.
library/core/src/iter/adapters/fuse.rs	Adds Kani harnesses for `Fuse::__iterator_get_unchecked`.
library/core/src/iter/adapters/filter.rs	Adds bounded + inductive-step Kani harnesses for `next_chunk`-related unsafe operations.
library/core/src/iter/adapters/filter_map.rs	Adds bounded + inductive-step Kani harnesses for `next_chunk`-related unsafe operations.
library/core/src/iter/adapters/enumerate.rs	Adds Kani harnesses for `Enumerate::__iterator_get_unchecked`.
library/core/src/iter/adapters/copied.rs	Adds Kani harnesses for `Copied::__iterator_get_unchecked` and `next_chunk` specialization.
library/core/src/iter/adapters/cloned.rs	Adds a safety contract for `next_unchecked` and Kani harnesses for unsafe methods.
library/core/src/iter/adapters/array_chunks.rs	Adds comments about loop reasoning and Kani harnesses for `next_back` and bounded `fold`.

Copilot · 2026-03-31T22:25:11Z

library/core/src/iter/adapters/zip.rs

@@ -1,4 +1,4 @@
-use safety::requires;
+use safety::{loop_invariant, requires};


loop_invariant is imported from safety but not used anywhere in this module (all loop invariants are written as #[cfg_attr(kani, kani::loop_invariant(...))]). This will trigger an unused_imports warning; either remove the import or switch the attributes to use the imported macro/path consistently.

Suggested change

use safety::{loop_invariant, requires};

use safety::requires;

Copilot · 2026-03-31T22:25:13Z

library/core/src/iter/adapters/zip.rs

    }

    #[inline]
+    #[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]


The #[requires(self.index + idx < ...)] contract can overflow on self.index + idx. In debug builds that can panic, and in release it can wrap and make the precondition unsound. Consider rewriting the contract to avoid overflowing arithmetic (e.g., require self.index <= a.size() and idx < a.size() - self.index, similarly for b), or use checked_add in the condition.

Suggested change

#[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]

#[requires(

self.index <= self.a.size()

&& idx < self.a.size() - self.index

&& self.index <= self.b.size()

&& idx < self.b.size() - self.index

)]

Copilot · 2026-03-31T22:25:14Z

library/core/src/iter/adapters/zip.rs

+        // Loop invariant: get_unchecked is a read-only operation for
+        // TrustedRandomAccessNoCoerce iterators, so sizes are preserved.
+        // Loop invariant enables loop contracts for unbounded verification.
+        // Safety of get_unchecked(i) is established by the pre-loop state:
+        // len = min(a.size(), b.size()) - index, and get_unchecked adds index
+        // back, so the actual index is always < both sizes.


These comments describe specific loop invariants about sizes and index bounds, but the attached Kani invariant is true (vacuous) and doesn’t actually encode those properties. To avoid misleading future readers, either encode the stated invariant(s) in the attribute expression, or adjust the comment to clarify that the invariant is intentionally vacuous and only used to enable loop-contract mode.

Suggested change

// Loop invariant: get_unchecked is a read-only operation for

// TrustedRandomAccessNoCoerce iterators, so sizes are preserved.

// Loop invariant enables loop contracts for unbounded verification.

// Safety of get_unchecked(i) is established by the pre-loop state:

// len = min(a.size(), b.size()) - index, and get_unchecked adds index

// back, so the actual index is always < both sizes.

// For TrustedRandomAccessNoCoerce iterators, get_unchecked is a

// read-only operation, so sizes are preserved.

// Safety of get_unchecked(i) is established by the pre-loop state:

// len = min(a.size(), b.size()) - index, and get_unchecked adds index

// back, so the actual index is always < both sizes.

// The Kani loop invariant below is intentionally vacuous (`true`) and

// is used only to enable loop-contract mode, not to encode these

// bounds or size properties directly.

Copilot · 2026-03-31T22:25:16Z

library/core/src/iter/adapters/take.rs

+use safety::loop_invariant;
+


loop_invariant is imported from safety but the file only uses #[cfg_attr(kani, kani::loop_invariant(...))] attributes. This causes an unused_imports warning; remove the import or use it consistently in the attributes.

Suggested change

use safety::loop_invariant;

Copilot · 2026-03-31T22:25:16Z

library/core/src/iter/adapters/take.rs

+        // Loop invariant: __iterator_get_unchecked is a read-only operation for
+        // TrustedRandomAccess iterators, so iter.size() is preserved across iterations.
+        #[cfg_attr(kani, kani::loop_invariant(true))]
        for i in 0..end {


The comment claims a loop invariant about iter.size() being preserved, but the Kani invariant provided is true (vacuous) and doesn’t encode that property. Either express the intended invariant in the attribute (so the comment matches what’s checked) or reword the comment to state that the invariant is intentionally trivial and only enables loop-contract verification.

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

library/core/src/iter/adapters/array_chunks.rs

+        // Loop invariant: __iterator_get_unchecked is read-only for
+        // TrustedRandomAccessNoCoerce iterators, so iter.size() is preserved.
+        // Loop invariant: i tracks the consumed element count and stays within


These lines are written as “Loop invariant: …”, but there’s no corresponding #[cfg_attr(kani, kani::loop_invariant(...))] annotation on the while loop. If this is meant to be a verified invariant, consider adding the attribute; otherwise, reword as a safety argument (to avoid implying the property is being checked).

Suggested change

// Loop invariant: __iterator_get_unchecked is read-only for

// TrustedRandomAccessNoCoerce iterators, so iter.size() is preserved.

// Loop invariant: i tracks the consumed element count and stays within

// Safety argument: __iterator_get_unchecked is read-only for

// TrustedRandomAccessNoCoerce iterators, so iter.size() is preserved.

// Safety argument: i tracks the consumed element count and stays within

kasimte requested a review from a team as a code owner February 19, 2026 01:43

kasimte force-pushed the challenge-16 branch 3 times, most recently from 68e2629 to c1620b6 Compare February 27, 2026 21:58

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

kasimte mentioned this pull request Mar 26, 2026

Test CI: Challenge 16 updates kasimte/verify-rust-std#2

Open

kasimte force-pushed the challenge-16 branch from c1620b6 to cee43ec Compare March 30, 2026 16:06

kasimte force-pushed the challenge-16 branch from cee43ec to 6cca1ff Compare March 30, 2026 16:23

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

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

Copilot AI reviewed Mar 31, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Verify safety of iterator adapter functions (Challenge 16)#549

Verify safety of iterator adapter functions (Challenge 16)#549
kasimte wants to merge 1 commit intomodel-checking:mainfrom
kasimte:challenge-16

kasimte commented Feb 19, 2026 •

edited

Loading

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!

Copilot AI Mar 31, 2026

Uh oh!

Copilot AI Mar 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		@@ -1,4 +1,4 @@
		use safety::requires;
		use safety::{loop_invariant, requires};

-    #[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]
+    #[requires(
+        self.index <= self.a.size()
+            && idx < self.a.size() - self.index
+            && self.index <= self.b.size()
+            && idx < self.b.size() - self.index
+    )]

Conversation

kasimte commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Requirements checklist

Known limitations

Source code modifications

Quick verification

Unbounded verification techniques

Safety contracts

Unsafe functions (10/10)

Safe abstractions (17/17)

Test plan

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

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!

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

kasimte commented Feb 19, 2026 •

edited

Loading