Verify safety of iterator adapter functions (Challenge 16)

[kasimte]

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

75 Kani harnesses verifying the safety of all 10 unsafe functions and all 17 safe abstractions across 13 iterator adapter files in library/core/src/iter/adapters/. Most of the unsafe-method #[requires] preconditions already exist upstream (added in #435); main has no harnesses for these adapters, so they are not yet machine-checked. This PR adds that verification layer — the harnesses that exercise each precondition and check the guarded get_unchecked/next_unchecked for UB. Loop-based paths carry loop-contract invariants that bound the iteration index, so Kani abstracts those loops instead of unwinding them — removing the per-harness unwind bound on those loops. Harness input arrays are bounded at MAX_LEN (5000 for u8; 50 for char/tuple; isize::MAX for the ZST); the zip::spec_fold inductive-step harness is the one arbitrary-length case. Per-function status is in the tables below.

Requirements checklist

Requirement	Status	Notes
All 10 unsafe functions	Done	Per-function harnesses verify each is UB-free under its precondition (Zip::get_unchecked exercised transitively via next/nth/fold). Of the 10 #[requires], 7 are upstream (#435); this PR adds 2 and rewrites Skip's in overflow-safe form
All 17 safe abstractions	Done	39 harnesses across 8 adapter files (incl. a checked #[ensures] contract for original_step via proof_for_contract)
Unbounded (arbitrary-length slices)	Partial — see Known limitations	Loop contracts remove unwinding bounds where annotated; input arrays are bounded at MAX_LEN except ZST (isize::MAX) and the spec_fold inductive step. We defer to the committee on whether this satisfies the criterion.
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). We defer to the committee's judgment.
Absence of UB	Done	CBMC checks pointer validity, uninitialized reads, immutable mutation, invalid values automatically
Safety contracts	Done	The 10 trait-impl #[requires] (7 upstream from #435, 2 added here, 1 rewritten overflow-safe) are precondition documentation, each mirrored by a kani::assume in the harness that exercises it — since proof_for_contract cannot resolve trait-impl methods, that harness is where they first get verified; the inherent original_step carries a checked #[ensures] via proof_for_contract

Known limitations

• Input-domain bounds: most harnesses draw symbolic slices from fixed-size arrays (MAX_LEN above), so slice length is symbolic only within that bound. The loop-contract annotations remove the unwinding bounds (Kani abstracts those loops); they do not make the input arrays arbitrary-length.

• array_chunks::fold: Bounded harness (MAX_LEN=8, unwind 9), N=2/u8 only. The TrustedRandomAccessNoCoerce-specialized fold path calls from_fn, whose internal MaybeUninit loop conflicts with loop-contract mode, so no source-level loop invariant is applied here. The unsafe operation — __iterator_get_unchecked(i + local) guarded by inner_len - i >= N — is the same indexed-access pattern abstracted 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 a single generic proof is not possible with this tool. The unsafe operations depend on size_of::<T>() and align_of::<T>(), not type identity; the 4 types cover those axes (integer, ZST, validity-constrained, padded). We defer to the committee on whether this satisfies the requirement.

Source code modifications

Five loop-contract invariants via #[cfg_attr(kani, kani::loop_invariant(...))], all verified inductive (base + step):

• take.rs spec_fold and spec_for_each: kani::index <= end
• zip.rs fold: kani::index <= len; nth: self.index <= end; super_nth: self.index <= self.len

Zero impact on non-Kani builds. Contract changes vs main: 7 of the 10 #[requires] are upstream (#435) and left unchanged; this PR adds 2 (Cloned::next_unchecked, Zip::get_unchecked), rewrites Skip::__iterator_get_unchecked's precondition in overflow-safe subtraction form, and adds 1 checked #[ensures] on the inherent original_step via proof_for_contract. The trait-impl #[requires] are precondition documentation (proof_for_contract cannot resolve trait-impl methods); each is mirrored by a kani::assume in the verify:: harness that exercises it — which is where the preconditions first get checked, as main carries them without a harness.

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 - 75 successfully verified harnesses, 0 failures, 75 total.

Verification techniques

1. 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].
2. Loop contracts — real invariants (kani::index <= end/len, self.index <= end) on the annotated loops in take.rs and zip.rs; Kani abstracts these loops, so no per-harness unwind bounds are needed for them.
3. Single-call pattern — For functions where unsafe ops are bounded by a constant (not slice length).
4. Two-call pattern — MapWindows: 2 calls to next() exercise buffer init + ring buffer wrap.
5. Inductive decomposition — an inductive-step harness verifies the unsafe ops are UB-free at a symbolic iteration k (unbounded in k), supplemented by bounded end-to-end harnesses. Used for zip::spec_fold, filter::next_chunk_dropless, filter_map::next_chunk.
6. Checked contracts where resolvable — StepBy::original_step (inherent method): #[ensures] + #[kani::proof_for_contract].

Safety contracts

Function	File	Contract	Source
__iterator_get_unchecked	cloned.rs	#[requires(idx < self.it.size_hint().0)]	upstream (#435)
next_unchecked	cloned.rs	#[requires(self.it.size_hint().0 > 0)]	added here
__iterator_get_unchecked	copied.rs	#[requires(idx < self.it.size_hint().0)]	upstream (#435)
__iterator_get_unchecked	enumerate.rs	#[requires(idx < self.iter.size_hint().0)]	upstream (#435)
__iterator_get_unchecked	fuse.rs	#[requires(self.iter.is_some() && idx < self.iter.as_ref().unwrap().size_hint().0)]	upstream (#435)
__iterator_get_unchecked	map.rs	#[requires(idx < self.iter.size_hint().0)]	upstream (#435)
next_unchecked	map.rs	#[requires(self.iter.size_hint().0 > 0)]	upstream (#435)
__iterator_get_unchecked	skip.rs	#[requires(self.n <= self.iter.size_hint().0 && idx < self.iter.size_hint().0 - self.n)]	rewritten overflow-safe (was #435)
__iterator_get_unchecked	zip.rs	#[requires(idx < self.size_hint().0)]	upstream (#435)
get_unchecked	zip.rs	#[requires(self.index <= self.a.size() && idx < self.a.size() - self.index && self.index <= self.b.size() && idx < self.b.size() - self.index)]	added here
original_step	step_by.rs	#[ensures(|result| result.get() - 1 == old(self).step_minus_one)] — checked via proof_for_contract	added here (checked)

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	4 above (called transitively via next/nth/fold)

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) + 1 contract proof (proof_for_contract)
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

• Changed-module harnesses (take, zip, skip, step_by) verified locally, with Kani built at the tool_config pin and the CI flag set.
• Full suite green in CI on this 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.

[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.

[kasimte]

Hi @feliperodri — addressed the Copilot review in commit e80e689:

• Removed unused loop_invariant imports in take.rs and zip.rs
• Rewrote Zip::get_unchecked #[requires(...)] to avoid self.index + idx overflow
• Clarified that the loop invariants on take.rs / zip.rs fold/spec_fold are intentionally vacuous (true only enables loop-contract mode)
• Reworded "Loop invariant:" → "Safety argument:" in array_chunks.rs for the un-annotated while loop

All CI green on the fork test PR kasimte#2 (identical tree). Ready for another look when you have a moment.

[Copilot]

Pull request overview

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

[kasimte]

Thanks for bringing the branch up to date with main, @feliperodri. Status: CI green, all six Copilot items resolved in e80e6899fc3. Ready for another look whenever it's convenient — happy to rebase or make any changes that'd help it land.

[Copilot]

Pull request overview

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

[feliperodri]

@kasimte This is strong, honest work — thank you for the transparent write-up of every limitation. To be clear up front about what's good: the source code is verified directly (no #[cfg(not(kani))] body substitution), and the unsafe trait-method harnesses are sound and non-circular — e.g. check_copied_get_unchecked_u8 does kani::assume(idx < iter.size_hint().0) (the documented precondition, not the safety conclusion), then lets CBMC check the real __iterator_get_unchecked(idx) for UB and asserts result == slice[idx]. That's a legitimate manual stand-in for proof_for_contract, and the #[requires] clauses faithfully match the assumed preconditions.

I'm requesting changes on two points.

1. The 5 loop_invariant(true) annotations (take.rs, zip.rs)

All five added loop invariants are #[cfg_attr(kani, kani::loop_invariant(true))], and the code comments call them "intentionally vacuous ... only to enable loop-contract mode." The concern: these loops perform get_unchecked(i) / __iterator_get_unchecked(i), whose safety depends on the induction variable staying < len. A true invariant does not establish that inductive bound, which leaves two possibilities that need to be resolved:

• If loop-contract mode genuinely abstracts the loop, the havoc'd i is constrained only by true, so the indexed access is exercised at an arbitrary index — the proof should then either fail or be relying on something else to re-derive the bound. Please explain why it's sound.
• If instead the loop is effectively still being unwound (bounded by MAX_LEN), then these functions are bounded, not "unbounded via loop contracts" as the summary states — in which case the claim should be corrected.

Either way, please provide a meaningful loop invariant that captures the bound the get_unchecked relies on (e.g. i <= len / self.index <= self.len), as you did locally for array_chunks::fold, or a concrete justification that true is sufficient and the coverage is genuinely unbounded. (This is the same trivial-invariant issue that #327's loop_invariant(true) and the discussion on #544 ran into.)

2. Decorative safety contracts (9 of 10 #[requires])

9 of the 10 #[requires(...)] (the __iterator_get_unchecked / get_unchecked trait methods) have no #[kani::proof_for_contract], so Kani never checks them as contracts — a plain #[kani::proof] that calls the method ignores its contract. I understand proof_for_contract doesn't support trait-impl methods today, and that you mirror each precondition with a kani::assume in a real harness (which is what actually does the verification). That's reasonable, but as written the annotation and the assumed precondition are independent and can silently drift. Please either:

• add a brief note in the code that these #[requires] are documentation-only (verification is via the mirrored assume in mod verify), and/or
• keep a single source of truth so the contract and the harness precondition can't diverge.

Minor / for the committee

The disclosed limitations — bounded array_chunks::fold, Range<u8> substitution for next_back_remainder, and 4 concrete types standing in for a generic T — are reasonable and clearly documented; I'll defer to the maintainers on whether they satisfy the "unbounded" and "generic" wording of the challenge.

Overall this is close, and the verification approach is sound where it counts. Resolving the loop-invariant question (item 1) is the main blocker.

[kasimte]

Thanks for the thorough review, @feliperodri — working through both items now (meaningful invariants + the requires notes); will push updates and a full response shortly.

[kasimte]

Thanks for the detailed review, @feliperodri. Both items are addressed in the pushed commits; details below.

1. Loop invariants (the 5 loop_invariant(true) sites)

You gave a choice between a meaningful loop invariant and a justification that true is sufficient; we took the first, at all five sites. Each now carries a real bound that verifies with base + step inductiveness checks passing:

Site	Invariant now
take.rs spec_fold / spec_for_each	kani::index <= end
zip.rs TRANC fold	kani::index <= len
zip.rs TRA nth	self.index <= end
zip.rs super_nth	self.index <= self.len

(kani::index is Kani's handle for a for loop's iteration count, per the loop-contracts reference; the loop's own pattern variable is not in scope in the invariant position.)

On your question of why the abstracted loop with true was sound rather than failing at an arbitrary index: the loops are genuinely abstracted, not unwound — the loop_invariant base/step checks appear in the verification output — and Kani retains the loop guard around the abstracted body (loop-contracts reference), so the havoc'd index stays < end and get_unchecked(i) was only ever checked under that bound. The explicit invariants now state that bound directly, so it is visible in the annotation and any drift is checkable.

2. Trait-impl #[requires]

Most of these #[requires] are already upstream (#435); because they sit on trait-impl methods, proof_for_contract cannot check them there, so they remain unchecked in main. This PR's harnesses are what exercise them: each #[requires] now carries a note that it documents the precondition and is verified via the mirrored kani::assume in the named verify:: harness, with the two to be kept in sync. I re-checked each assume against its contract expression and found them consistent.

Where proof_for_contract can resolve the method — the inherent StepBy::original_step — this push adds #[ensures(|result| result.get() - 1 == old(self).step_minus_one)] with a proof_for_contract harness. Skip::__iterator_get_unchecked's precondition is also rewritten in the overflow-safe subtraction form, matching the Zip::get_unchecked fix.

Claim corrections

The PR body and the harness comments now separate the two axes: loop contracts remove the unwinding bounds on the annotated loops, while harness input arrays remain bounded at MAX_LEN (5000/u8, 50/char+tuple; ZST at isize::MAX; the spec_fold inductive step is the arbitrary-length case). "unbounded" now appears only where it is literally true, and the requirements table leaves the criterion judgment to the committee.

Also in this push

• Merged current main (nightly-2025-11-25 subtree update); no runtime-logic changes to the 27 target functions.
• CI on the updated branch: green — all Verify std partitions, autoharness, and upstream_test (rustfmt) passing.

The remaining gaps — input-domain bounds and concrete types for T — are disclosed in the body; glad to track them however the committee prefers.