Verify iter adapter unsafe methods + safe abstractions (challenge #16)

[MavenRain]

Challenge 16: Verify the safety of core::iter adapters

Towards challenge #16 (tracking issue #280). Adds Kani harnesses for the unsafe
methods and safe abstractions in library/core/src/iter/adapters/.

This revision answers the 2026-08-15 review (feliperodri: CHANGES_REQUESTED,
blockers F-B1 unbounded and F-B2 generic T, plus notes F-N1..F-N5; Copilot:
the same points inline, plus the enumerate.rs doc comment). Section "Response
to review" below goes item by item. Section "std code changes" lists every
line changed outside the #[cfg(kani)] mod verify modules. Section "Harness
inventory" lists every harness with its bound and element types. Section
"Known upstream findings" lists the two defects the harnesses found in the
current upstream code and how the harness domains exclude them.

Unsafe methods (proven free of UB)

adapter	unsafe methods
cloned	__iterator_get_unchecked, next_unchecked
copied	__iterator_get_unchecked
enumerate	__iterator_get_unchecked
fuse	__iterator_get_unchecked
map	__iterator_get_unchecked, next_unchecked
skip	__iterator_get_unchecked (plain source, and a MAY_HAVE_SIDE_EFFECT = true source)
zip	__iterator_get_unchecked, and ZipImpl::get_unchecked directly over arbitrary valid Zip state

The __iterator_get_unchecked harnesses read at a symbolic in-bounds index
(kani::any_where(|i| i < size_hint().0)) over a kani::any() backing array;
the next_unchecked harnesses establish the non-empty precondition by
construction.

Safe abstractions (proven free of UB)

array_chunks::next_back_remainder and array_chunks::fold,
copied::spec_next_chunk, filter::next_chunk_dropless,
filter_map::next_chunk, the map_windows Buffer operations (as_array_ref,
as_uninit_array_mut, push, drop), step_by::original_step,
take::spec_fold and take::spec_for_each, and zip::next / next_back /
nth / fold / spec_fold.

Approach

• Harnesses live in a #[cfg(kani)] mod verify at the end of each adapter file.
• Because Kani cannot attach a proof_for_contract to a generic trait method
  (kani#1997), each generic method is instantiated at representative concrete
  element types via macros, with the caller precondition established by
  construction rather than as a #[requires].
• The representative element types are unit (ZST), u8 (1-byte), char (4-byte,
  validity-constrained), compound tuples with padding such as (char, u8) and
  (u32, i16), and, where a code path is gated on needs_drop, a DropToken
  type with a real destructor; zip harnesses pair two of them.
• The per-element loops in the production code that the harnesses drive carry
  #[safety::loop_invariant(...)] (the repo's loop-contract spelling, already
  used on plain for loops in slice/mod.rs, str/pattern.rs,
  num/dec2flt/decimal_seq.rs), so the iterating harnesses have no
  #[kani::unwind] for those loops and the slice length is symbolic instead of
  unrolled. The invariants bound only the loop counter, because the loop
  frame Kani infers (or, for array_chunks, the frame stated with
  kani::loop_modifies) writes only the counter and the accumulator, so every
  size relation the body needs survives as an entry value. Where a loop
  cannot take a contract (it calls next on a generic inner iterator, or it
  lives in the generic Iterator::try_fold default), the harness stays
  bounded and the code comment says why.
• No loop changed shape. Every production hunk is an added attribute, an
  added #[cfg(kani)] import, or an added comment.

Response to review

F-B1: unbounded verification

Status: the production loops that the harnesses drive now carry
#[safety::loop_invariant], and the corresponding harnesses have no
#[kani::unwind] for those loops (an unwind attribute is kept only where a
sibling construct with a length-independent trip count needs one, stated per
row). 23 loop-contract harnesses (take 8, array_chunks 4, zip 11:
fold x4, nth x4, nth side-effect x3) run with a symbolic slice length
and no unrolling depth on the contracted loop.
Two adapters (filter, filter_map) and four narrow
array_chunks/zip/skip paths stay bounded, for the reasons below. Local
run status is in "Verification status".

Now verified by a loop invariant on the production loop:

production loop	invariant	harnesses (unwind attribute)
take.rs SpecTake::spec_fold (TrustedRandomAccess impl), for i in 0..end	kani::index <= end	check_take_spec_fold_unit, check_take_spec_fold_u8, check_take_spec_fold_char, check_take_spec_fold_tup (none)
take.rs SpecTake::spec_for_each (TrustedRandomAccess impl), for i in 0..end	kani::index <= end	check_take_spec_for_each_unit, check_take_spec_for_each_u8, check_take_spec_for_each_char, check_take_spec_for_each_tup (none)
array_chunks.rs SpecFold::fold (TrustedRandomAccessNoCoerce impl), while inner_len - i >= N	i <= inner_len, with #[cfg_attr(kani, kani::loop_modifies(&accum, &i))]	check_array_chunks_fold_unit, check_array_chunks_fold_u8, check_array_chunks_fold_char, check_array_chunks_fold_tup (none)
zip.rs ZipImpl::fold (TrustedRandomAccessNoCoerce impl), for i in 0..len	kani::index <= len	check_zip_fold_unit, check_zip_fold_u8, check_zip_fold_char_u8, check_zip_fold_tup (none)
zip.rs ZipImpl::nth (TrustedRandomAccessNoCoerce impl), while self.index < end	self.index <= end	check_zip_nth_unit, check_zip_nth_u8 (unwind(3)), check_zip_nth_char_u8, check_zip_nth_tup (unwind(12)), check_zip_nth_side_effect_a, check_zip_nth_side_effect_b, check_zip_nth_side_effect_both (unwind(3)). The unwind attribute covers only super_nth, which runs at most one iteration after the contracted loop has consumed min(n, len - index) items, and (for char and the tuple) the element-wise kani::any construction of the MAX_LEN backing arrays; neither count depends on the slice length.

Why the invariants only bound the counter. The loop frame that Kani's loop
contract machinery infers for these loops is {acc, i} (or {accum, i}, or
{self.index} for zip::nth): end, len, self.iter, self.a, self.b
are not havoced, so end <= self.iter.size() and
end <= self.len <= min(a.size(), b.size()) stay available to the body as
entry values and do not need restating. A method call on the captured self
inside the invariant (for example self.iter.size() == ...) is not something
the current Kani/CBMC pipeline evaluates (it becomes a nondeterministic
value), so the counter-only form is both sufficient and the only form that
proves. For array_chunks::fold the frame is stated explicitly with
kani::loop_modifies(&accum, &i) (precedent: slice/mod.rs), because the
from_fn closure borrows self mutably and the inferred frame would
otherwise havoc the whole adapter, remainder included. Each production
comment says this.

What "unbounded" means here, stated precisely: the loop is verified by
invariant (CBMC havocs the loop frame and checks the invariant inductively),
so no unrolling depth truncates the number of iterations. The slice length is
still a symbolic value in 0..=MAX_LEN where MAX_LEN is the size of the
kani::any() backing array. For the loop-contract harnesses MAX_LEN is
isize::MAX for the ZST (every length a Rust slice can have; 50 for the
zip pair, whose two arrays are separate allocations), u32::MAX for u8,
and 10 for char and the padded tuples. The 10 is a solver-time choice, not
a proof-structure one: the loop is the same monomorphic code at every
MAX_LEN, and the cost that scales with MAX_LEN for the wide types is the
element-wise kani::any construction of the backing array under the
loop-contract (DFCC) transformation, not the loop. The ZST and u8
instantiations run the same contracted loop at isize::MAX / u32::MAX, so
the loop contract is exercised at full length there. If the committee wants
the char/tuple caps raised, that is a one-number change per macro
instantiation, at the price of longer runs.

Still bounded, and why:

• filter.rs next_chunk_dropless (8 harnesses, MAX_LEN = 6, unwind(7))
  and filter_map.rs next_chunk (12 harnesses, MAX_LEN = 5, unwind(6)).
  Both fill the chunk through the generic default Iterator::try_fold in
  iterator.rs (lines 2424-2435, a while let Some(x) = self.next() loop that
  calls a generic FnMut), so the adapter has no loop of its own to annotate,
  and the tree has no loop contract on the generic default; annotating
  iterator.rs is out of this challenge's scope. The fixed MAX_LEN is a
  complete cover of the reachable state space rather than a truncation: the
  only loop-carried state is initialized in 0..=N, so any MAX_LEN >= N + 2
  reaches every configuration (empty source, saturation before exhaustion,
  exhaustion before saturation). The code comment in each file says this.
• array_chunks.rs next_back_remainder (4 harnesses, MAX_LEN 8/8/9/8, no
  unwind attribute). The fill runs len % N < N steps whatever the slice
  length is, so MAX_LEN >= N plus the symbolic length covers every reachable
  remainder.
• zip.rs SpecFold::spec_fold (TrustedLen impl): check_zip_spec_fold_unit,
  _u8, _char_u8, _tup (MAX_LEN = 5, unwind(7)). The inner
  for _ in 0..upper calls next on the generic inner iterators, which moves
  their private pointer state; no public interface lets a loop invariant pin
  that state to its allocation, so a loop contract would havoc it into an
  unverifiable read. The outer loop runs once per usize::MAX chunk, so
  exactly once for these sources. The code comments at both loops say this.
• zip.rs specialized next_back length-adjust loops with side-effecting
  sources: check_zip_next_back_side_effect_a, _b, _both (MAX_LEN = 5,
  unwind(7)). Same blocking construct: next_back on the generic inner
  iterators. With plain slice::Iter sources (check_zip_next_back_unit,
  _u8, _char_u8, _tup) these loops are compiled out
  (MAY_HAVE_SIDE_EFFECT = false), so those four harnesses have no unwind
  attribute; they share the check_zip_safe! instantiation with the
  loop-contracted nth/fold siblings, so MAX_LEN is 50 / u32::MAX / 10 /
  10 (the same values as those siblings, not the accessor menu).
• skip.rs check_skip_get_unchecked_side_effect (MAX_LEN = 5,
  unwind(7)): the idx == 0 prefix-drop loop for skipped_idx in 0..self.n
  runs self.n times through try_get_unchecked on the inner Map, and
  self.n is symbolic up to the slice length, so this harness is bounded by
  MAX_LEN.
• zip.rs super_nth (while let Some(x) = Iterator::next(self)) and the
  generic (non-TrustedLen) SpecFold::spec_fold: no size relation is
  available to an invariant for a general Zip. super_nth is only reached
  after the contracted nth loop and runs at most one iteration (covered by
  the nth harnesses' unwind attribute); the generic spec_fold is not
  selected for any harnessed source (all are TrustedLen). Both carry a
  comment saying so.

The remaining harnesses (__iterator_get_unchecked / next_unchecked
accessors, copied::spec_next_chunk which is a single bulk copy,
step_by::original_step, the map_windows Buffer operations) have no
per-element loop; they were never unwind-bounded and are unchanged except for
copied::spec_next_chunk, whose MAX_LEN is raised from 16 to the accessor
menu.

F-B2: generic T

Kani monomorphizes: every harness is a concrete entry point, and CBMC verifies
GOTO for concrete types, so a Kani proof "over T" is always a proof over the
set of instantiations the harnesses request. What the harnesses can do is pick
that set so that it spans every property of T the unsafe code can observe.
The code under proof reads T only through size_of, align_of, validity of
the bit pattern, and needs_drop; it never branches on T's identity. The
menu:

• (): ZST. Size 0 and align 1, so every pointer arithmetic degenerates and
  the "no allocation" edge is exercised.
• u8: the trivial 1-byte, no-niche, no-padding case.
• char: 4-byte, aligned, with invalid bit patterns. kani::any::<char>()
  is a filtered map over u32 (it assumes the scalar is a valid char), so a
  read that lands on padding, uninitialized memory, or a foreign slot surfaces
  as a validity failure instead of passing silently.
• (char, u8) (and (u32, i16) on the second zip side): compound with
  interior padding, so byte-wise copies and MaybeUninit slots carry
  uninitialized bytes.
• DropToken (a u8 newtype with a Drop impl that reads its payload) on the
  paths gated by needs_drop: map_windows::Buffer (push's drop_in_place
  and the Drop impl) and filter_map::next_chunk (the Guard), so real drop
  glue is compiled in and every dropped slot must be live and in bounds.

This is the same menu the accessor harnesses in enumerate.rs and
copied.rs of this PR already used, and it is applied uniformly to the
loop-contract harnesses now. A universally quantified proof over T is not
expressible in Kani (kani#1997 for the contract side; CBMC's model on the
solver side), so this is representative-instantiation coverage; the PR states
that plainly rather than claiming otherwise, and the "Honest caveats" note
about monomorphization is kept below.

F-doc: enumerate.rs doc comments

Both comments Copilot flagged (and the one feliperodri flagged) are corrected:
the any_slice doc no longer says the sub-slice "makes the proof unbounded";
it now says the length is symbolic in 0..=MAX_LEN and that the proof is
still bounded by MAX_LEN (with the u32::MAX/isize::MAX vs 50 split
spelled out). The macro doc no longer says "proof_for_contract ... the
contract itself stays generic"; it says one plain #[kani::proof] per
concrete type and points at the NOTE that explains kani#1997. The
"Bounded MAX_LEN because the methods iterate" comments in take.rs,
array_chunks.rs and zip.rs are replaced by the loop-contract wording.

F-N1: direct ZipImpl::get_unchecked proof

New macro check_zip_get_unchecked_direct (5 harnesses:
check_zip_get_unchecked_direct_unit_unit, _u8_u8, _char_u8, _u8_char,
_tup_tup). It builds Zip { a, b, index, len } directly with symbolic
len <= min(a.len(), b.len()) and symbolic index <= len (every state
reachable from the TrustedRandomAccess constructor, since next only
increments index and next_back only decrements len), picks
idx < len - index (the method's caller contract, idx < size_hint().0), and
calls ZipImpl::get_unchecked(&mut it, idx). This proves self.index + idx
stays in bounds of both sources and cannot overflow, on index > 0 states as
well. The transitive __iterator_get_unchecked harnesses stay. All five are
SUCCESSFUL locally.

F-N2: MAY_HAVE_SIDE_EFFECT = true sources

map.rs pins MAY_HAVE_SIDE_EFFECT = true for every
Map<I, F>: TrustedRandomAccessNoCoerce, so Map<slice::Iter<u8>, fn(&u8) -> u8>
is a side-effecting TrustedRandomAccess source without any test-only model.

• skip.rs: check_skip_get_unchecked_side_effect wraps that Map in
  Skip with symbolic n <= slice.len() and symbolic idx, so the
  if Self::MAY_HAVE_SIDE_EFFECT && idx == 0 branch is compiled in and covered
  both taken (idx == 0, dropping the n skipped items) and not taken.
• zip.rs: check_zip_side_effect! instantiated for the Map on side a,
  side b, and both (check_zip_nth_side_effect_a/_b/_both,
  check_zip_next_back_side_effect_a/_b/_both), so the
  A::MAY_HAVE_SIDE_EFFECT / B::MAY_HAVE_SIDE_EFFECT branches of the
  specialized nth and next_back (including next_back's length-adjust
  loops) are compiled in. The two any_slice lengths are independent, so the
  sz_a != sz_b adjust path is reachable.
• One shape is excluded from the next_back side-effect harnesses, and the
  exclusion is a finding rather than a gap: with exactly one side-effecting
  side, and that side shorter than the plain side, upstream's
  debug_assert_eq!(self.a.size(), self.b.size()) after the trim step fires
  (the trim loops only run for the MAY_HAVE_SIDE_EFFECT side, so the plain
  longer side is never trimmed). Kani reports it as a failed assertion in a
  debug build. The macro takes a $back_shape predicate
  (len_a >= len_b for _a, len_b >= len_a for _b, true for _both),
  the code comment says why, and the defect is reported upstream (see "Known
  upstream findings"). The nth side-effect harnesses have no such
  exclusion.

F-N3: map_windows drop-safety path

verify_map_windows_drop instantiates check_buffer! at DropToken
(needs_drop true), so push's drop_in_place and the Buffer Drop impl
execute real drop glue whose destructor reads the payload; every dropped slot
must be an in-bounds, live slot. Caveat, also in the code comment: Kani
models a panic as a verification failure and has no unwinding, so the
panic-during-drop ordering argument ("update start before drop_in_place")
is not expressible as a passing harness; the coverage this adds is the
non-trivial drop-glue path.

F-N4: filter_map output types

maybe_map is replaced by maybe_map_to<T, B: kani::Arbitrary> and the macro
takes the output type. The 8 existing harnesses keep B = usize; four new
harnesses cover B = char, (), (char, u8), and DropToken
(check_filter_map_next_chunk_out_char/_out_unit/_out_tup/_out_drop). With
DropToken, needs_drop::<B>() is true, so the Guard::drop path is
compiled in as the comment claims.

F-N5: N = 0

N = 0 is excluded on purpose, and the reason is now a finding rather than an
omission. Kani confirms an out-of-bounds write in the current upstream code:
Filter::next_chunk_dropless::<0> writes through
array.get_unchecked_mut(idx) before it compares initialized < N, and
FilterMap::next_chunk::<0> does a one-element copy_nonoverlapping into
guard.array at idx before it compares guard.initialized < N; on any
source that yields at least one element, both write into a zero-capacity
array (Kani 0.65.0: 6 of 272 checks failed for filter, 1 of 294 for
filter_map). doc/src/general-rules.md does not permit a local change to
runtime logic, so the fix must land upstream: rust-lang/rust issue
<>. The harnesses cover N >= 1; N = 1 harnesses
(*_n1, the smallest valid capacity) are added next to the N = 4 (filter)
and N = 3 (filter_map) ones. Once the upstream fix lands and is merged
here, N = 0 instantiations are a one-line addition per macro.

std code changes (outside mod verify)

Every production line touched, with the reason. All are runtime no-ops:
#[safety::loop_invariant] expands to nothing outside Kani
(library/contracts/safety/src/runtime.rs returns the statement unchanged),
#[cfg_attr(kani, ...)] and #[cfg(kani)] items are compiled out, and the
rest are comments. No loop changed shape. Precedent for a
loop_invariant on a plain for loop with kani::index:
slice/mod.rs:1014-1019 (also the loop_modifies precedent),
str/pattern.rs:1974, num/dec2flt/decimal_seq.rs:108.

file:lines	change	why	runtime effect
array_chunks.rs:6-7	#[cfg(kani)] use crate::kani;	brings kani::loop_modifies into scope	none (cfg-gated import)
array_chunks.rs:235-242	6 comment lines, #[safety::loop_invariant(i <= inner_len)], #[cfg_attr(kani, kani::loop_modifies(&accum, &i))] on the existing while inner_len - i >= N loop in SpecFold::fold	unbounded fold harnesses; the explicit frame keeps the from_fn closure's &mut self borrow from havocing remainder	none
take.rs:4-5	#[cfg(kani)] use crate::kani;	brings kani::index into scope	none (cfg-gated import)
take.rs:304-308	4 comment lines + #[safety::loop_invariant(kani::index <= end)] on the existing for i in 0..end in SpecTake::spec_fold (TrustedRandomAccess impl)	unbounded spec_fold harnesses	none
take.rs:320-321	1 comment line + #[safety::loop_invariant(kani::index <= end)] on the existing for i in 0..end in SpecTake::spec_for_each	unbounded spec_for_each harnesses	none
zip.rs:31-36	comment in super_nth: why this loop stays bounded	documents the bound	none
zip.rs:294-298	4 comment lines + #[safety::loop_invariant(kani::index <= len)] on the existing for i in 0..len in the TrustedRandomAccessNoCoerce ZipImpl::fold	unbounded fold harnesses	none
zip.rs:348-352	4 comment lines + #[safety::loop_invariant(self.index <= end)] on the existing while self.index < end in the TrustedRandomAccessNoCoerce ZipImpl::nth	unbounded nth harnesses	none
zip.rs:405-411	comment in the specialized next_back: why the two adjust loops stay bounded	documents the bound	none
zip.rs:681-684	comment in the generic SpecFold::spec_fold: why the while let stays bounded	documents the bound	none
zip.rs:699-702	comment on the outer loop of the TrustedLen SpecFold::spec_fold	documents the bound	none
zip.rs:711-716	comment on the inner for _ in 0..upper of the TrustedLen SpecFold::spec_fold: why it stays bounded	documents the bound	none

Harness inventory

Bound column: "invariant" means the production loop carries a
#[safety::loop_invariant] and the harness has no unwind attribute (or one
that only covers a length-independent sibling construct, stated); "no loop"
means the harness drives no per-element loop and has no unwind attribute;
"unwind(N)" means bounded finite unrolling with the stated MAX_LEN.
MAX_LEN menu "accessor" = isize::MAX for (), u32::MAX for u8, 50 for
char and (char, u8); "loop-contract" = isize::MAX for (), u32::MAX
for u8, 10 for char and (char, u8). zip pairs use 50 for the ZST
pair.

file	harnesses	bound	element types
cloned.rs	check_cloned_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	(), u8, char, (char, u8)
cloned.rs	check_cloned_next_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
copied.rs	check_copied_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
copied.rs	check_copied_spec_next_chunk_unit/_u8/_char/_tup (N = 2/3/2/2)	no loop (bulk copy), accessor MAX_LEN (raised from 16)	same
enumerate.rs	check_enumerate_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
fuse.rs	check_fuse_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
map.rs	check_map_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
map.rs	check_map_next_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same
skip.rs	check_skip_get_unchecked_unit/_u8/_char/_tup	no loop, accessor MAX_LEN	same (plain slice::Iter)
skip.rs	check_skip_get_unchecked_side_effect	unwind(7), MAX_LEN = 5 (prefix-drop loop runs symbolic n times)	u8 via Map<slice::Iter<u8>, fn>
step_by.rs	check_step_by_original_step_unit/_u8/_char/_tup	no loop, MAX_LEN = 16 (proof is over symbolic step)	(), u8, char, (char, u8)
map_windows.rs	verify_map_windows_unit/_u8/_char/_tup/_drop::{check_as_array_ref, check_as_uninit_array_mut, check_push, check_drop} (N = 3/3/2/2/2)	no slice; N is the const generic, no unwind attribute	(), u8, char, (char, u8), DropToken
array_chunks.rs	check_array_chunks_next_back_remainder_unit/_u8/_char/_tup (N = 2/2/3/2)	MAX_LEN 8/8/9/8, no unwind attribute (fill runs len % N < N steps)	(), u8, char, (char, u8)
array_chunks.rs	check_array_chunks_fold_unit/_u8/_char/_tup (N = 2/2/3/2)	invariant (+ loop_modifies frame), loop-contract MAX_LEN	same
take.rs	check_take_spec_fold_unit/_u8/_char/_tup	invariant, loop-contract MAX_LEN	same
take.rs	check_take_spec_for_each_unit/_u8/_char/_tup	invariant, loop-contract MAX_LEN	same
filter.rs	check_filter_next_chunk_dropless_unit/_u8/_char/_tup (N = 4) and ..._unit_n1/_u8_n1/_char_n1/_tup_n1 (N = 1)	unwind(7), MAX_LEN = 6 (default try_fold; complete state cover)	same
filter_map.rs	check_filter_map_next_chunk_unit/_u8/_char/_tup (N = 3, out usize), ..._unit_n1/_u8_n1/_char_n1/_tup_n1 (N = 1, out usize), check_filter_map_next_chunk_out_char/_out_unit/_out_tup/_out_drop (in u8, N = 3)	unwind(6), MAX_LEN = 5 (default try_fold; complete state cover)	in: (), u8, char, (char, u8); out: usize, char, (), (char, u8), DropToken
zip.rs	check_zip_get_unchecked_unit_unit/_u8_u8/_char_u8/_u8_char/_tup_tup	no loop, MAX_LEN 50 / u32::MAX / 50 / 50 / 50	((),()), (u8,u8), (char,u8), (u8,char), ((char,u8),(u32,i16))
zip.rs	check_zip_get_unchecked_direct_unit_unit/_u8_u8/_char_u8/_u8_char/_tup_tup	no loop, same MAX_LEN menu; symbolic index <= len <= min	same pairs
zip.rs	check_zip_next_unit/_u8/_char_u8/_tup	no loop, MAX_LEN 50 / u32::MAX / 10 / 10	((),()), (u8,u8), (char,u8), ((char,u8),(u32,i16))
zip.rs	check_zip_nth_unit/_u8/_char_u8/_tup	invariant on nth; unwind(3)/(3)/(12)/(12) for super_nth and the wide-type kani::any array construction only; MAX_LEN 50 / u32::MAX / 10 / 10	same pairs
zip.rs	check_zip_next_back_unit/_u8/_char_u8/_tup	no loop (adjust loops compiled out for slice::Iter); MAX_LEN 50 / u32::MAX / 10 / 10	same pairs
zip.rs	check_zip_fold_unit/_u8/_char_u8/_tup	invariant on ZipImpl::fold; MAX_LEN 50 / u32::MAX / 10 / 10	same pairs
zip.rs	check_zip_spec_fold_unit/_u8/_char_u8/_tup	unwind(7), MAX_LEN = 5 (inner loop calls generic next; outer loop runs once)	same pairs
zip.rs	check_zip_nth_side_effect_a/_b/_both	invariant on nth; unwind(3) for super_nth only; MAX_LEN = u32::MAX	u8 / u8, one or both sides through Map<slice::Iter<u8>, fn>
zip.rs	check_zip_next_back_side_effect_a/_b/_both	unwind(7), MAX_LEN = 5 (adjust loops call generic next_back); $back_shape excludes the debug-assert shape (see F-N2)	same

Verification status

CI runs every harness through scripts/run-kani.sh (which passes
-Z loop-contracts alongside the other unstable flags). Local runs below use
Kani 0.65.0 with the same flag set (verify-std -Z unstable-options ./library -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12),
one harness per invocation, each on a fresh per-harness build of the current
tree.

Local, SUCCESSFUL, 2026-08-17 (loop-contract and zip sweep, 42 harnesses,
19-46 s wall each):

• take.rs: check_take_spec_fold_unit/_u8/_char/_tup and
  check_take_spec_for_each_unit/_u8/_char/_tup (8 of 8).
• array_chunks.rs: check_array_chunks_fold_unit/_u8/_char/_tup and
  check_array_chunks_next_back_remainder_unit/_u8/_char/_tup (8 of 8).
• zip.rs: check_zip_fold_unit/_u8/_char_u8/_tup,
  check_zip_nth_unit/_u8/_char_u8/_tup,
  check_zip_spec_fold_unit/_u8/_char_u8/_tup,
  check_zip_next_u8, check_zip_next_back_unit/_u8,
  check_zip_get_unchecked_direct_unit_unit/_u8_u8/_u8_char/_char_u8/_tup_tup,
  check_zip_nth_side_effect_a/_b/_both,
  check_zip_next_back_side_effect_a/_b/_both (26 of 26).

Local, SUCCESSFUL, 2026-08-17 (the remaining zip.rs harnesses, no loop
contract involved, re-run after the MAX_LEN menu change; 10 of 10, 20-36 s
wall each): check_zip_next_unit/_char_u8/_tup,
check_zip_next_back_char_u8/_tup,
check_zip_get_unchecked_unit_unit/_u8_u8/_u8_char/_char_u8/_tup_tup.
Every harness in zip.rs (36) is therefore green locally on the current
tree.

Local, SUCCESSFUL, 2026-08-16 (files not touched since):

• filter.rs: all 8 check_filter_next_chunk_dropless* harnesses (0 failed
  each; 271 to 563 checks per harness).
• filter_map.rs: all 12 check_filter_map_next_chunk* harnesses (0 failed
  each; 295 to 587 checks per harness).
• copied.rs: all 4 check_copied_spec_next_chunk* harnesses at the raised
  MAX_LEN (0 failed each).
• skip.rs: check_skip_get_unchecked_side_effect (0 of 222 failed).
• map_windows.rs: verify_map_windows_drop::{check_drop, check_push, check_as_uninit_array_mut, check_as_array_ref} (0 failed each).
• enumerate.rs: check_enumerate_get_unchecked_u8 after the comment edit
  (0 failed).

The accessor harnesses in cloned.rs, copied.rs (get_unchecked),
enumerate.rs (the other three), fuse.rs, map.rs, skip.rs (plain),
step_by.rs, and map_windows.rs (unit/u8/char/tup) are unchanged from
the previous revision, which CI verified; CI re-verifies them here.

Known upstream findings (excluded from the harness domains, issues to be filed)

Both are defects in the current upstream core code that Kani surfaced while
building these harnesses. Neither is fixed in this PR
(doc/src/general-rules.md: no local change to std runtime logic); each is
excluded from the harness domain with a code comment that names the
exclusion, and reported upstream.

1. Filter::next_chunk_dropless::<0> and FilterMap::next_chunk::<0> write
   one element into a zero-capacity array before the initialized < N
   check (out-of-bounds write on any non-empty source). Excluded by
   instantiating N >= 1 only. Issue: <>.
2. TrustedRandomAccess Zip::next_back:
   debug_assert_eq!(self.a.size(), self.b.size()) after the trim step fires
   when exactly one side has MAY_HAVE_SIDE_EFFECT = true and that side is
   the shorter one (the plain longer side is never trimmed). Debug-only
   false assertion, no UB in release. Excluded by the $back_shape
   assumption in check_zip_side_effect! (_a: len_a >= len_b; _b:
   len_b >= len_a; _both: no exclusion). Issue:
   <>.

Honest caveats (please review)

1. Monomorphization. Representative-instantiation coverage, not a single
   universal-over-T proof; the F-B2 answer above says why and which
   properties of T each instantiation pins. Glad to switch encodings if the
   committee prefers a different form.
2. Boundedness. The loops the harnesses drive are verified by invariant
   except the ones listed under "Still bounded, and why" (filter,
   filter_map, array_chunks::next_back_remainder, the TrustedLen
   zip::spec_fold, the side-effecting zip next_back and skip
   prefix-drop paths). For those, the code comment states the bound and the
   state-space argument, and the bound is a property of the generic default
   try_fold / private inner-iterator state, not of the adapter code.
3. MAX_LEN for wide element types. 10 for char and the tuples in the
   loop-contract harnesses (50 in the accessor harnesses) is a kani::any()
   array size, not an unrolling depth; the u8/ZST instantiations of the same
   loops run to u32::MAX/isize::MAX.
4. N = 0 for filter/filter_map. Excluded because upstream is
   currently unsound there (see F-N5); tracked upstream at
   <>.
5. zip::next_back with one side-effecting shorter side. Excluded
   because upstream's debug assertion is false there (see F-N2); tracked
   upstream at <>.

[MavenRain]

Status update for reviewers: this PR is green on every check and mergeable
against current main.

It covers the complete unsafe surface of the iter adapters: all
__iterator_get_unchecked, next_unchecked, and get_unchecked methods
across cloned, copied, enumerate, fuse, map, skip, and zip, plus the safe abstractions
listed in the description. Each generic trait method is verified at representative
concrete element types via macro instantiation, with the caller precondition
established by construction, since Kani cannot place contracts on generic trait
methods (kani#1997).

The one design decision worth a maintainer's eye is that kani#1997 workaround:
these use plain #[kani::proof] plus precondition-by-construction rather than
proof_for_contract, which proves the same no-UB property the contract would
express. Glad to switch encodings if you would prefer a different form.

The iterating adapters listed as deferred are already verified on a follow-up
branch; I can fold them into this PR or send them separately, whichever you
prefer. Thanks for taking a look whenever you have a chance.

[Copilot]

Pull request overview

Adds Kani-gated verification harnesses for Challenge 16’s iterator adapters. However, generic and unbounded verification requirements remain unmet, with additional uncovered edge cases.

Changes:

• Adds proofs for unsafe iterator accessors.
• Verifies safe adapter abstractions and buffer operations.
• Uses symbolic slices, representative types, and bounded loop unwinding.

Reviewed changes

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

Show a summary per file

File	Description
array_chunks.rs	Verifies remainder and fold operations.
cloned.rs	Covers unchecked cloning accessors.
copied.rs	Covers unchecked access and chunk copying.
enumerate.rs	Verifies unchecked enumerated access.
filter.rs	Checks dropless chunk construction.
filter_map.rs	Checks mapped chunk construction.
fuse.rs	Covers unchecked fused access.
map.rs	Covers unchecked mapped access.
map_windows.rs	Verifies internal buffer operations.
skip.rs	Covers unchecked skipped access.
step_by.rs	Verifies step reconstruction.
take.rs	Checks specialized fold operations.
zip.rs	Verifies unchecked and safe zip operations.

Suppressed comments (1)

library/core/src/iter/adapters/enumerate.rs:365

• Replacing contract proofs with concrete #[kani::proof] monomorphizations does not meet Challenge 16's explicit requirement that the result hold for generic T with no monomorphization. Representative size/alignment classes cannot cover type-dependent behavior such as drop glue and validity niches. This needs an accepted generic encoding or an explicit committee change to the challenge criteria before these harnesses can count as a solution.

    // NOTE: `__iterator_get_unchecked` is a trait method on the *generic* impl
    // `impl<I> Iterator for Enumerate<I>`, and Kani cannot attach a
    // `proof_for_contract` to a generic trait method (kani#1997).  So instead of
    // the contract machinery we use a plain `#[kani::proof]` that establishes the
    // method's precondition by construction (`idx < self.iter.size_hint().0`) and

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Review of PR #602 — Challenge 16 (iter adapters)

This is careful, honest, non-vacuous work. There is no fatal soundness problem: no cfg-swap vacuity (all verify modules are #[cfg(kani)]), no loop_invariant(true), and the unsafe-accessor harnesses use the correct pattern of assuming the documented precondition rather than the conclusion. Unfortunately it does not meet the two hard success criteria Challenge 16 states verbatim, so I cannot approve as-is.

Blocker 1 — "The verification must be unbounded—it must hold for slices of arbitrary length."

Every harness that actually iterates is bounded by a small fixed backing array plus #[kani::unwind(N)], so it proves nothing beyond that bound:

• array_chunks.rs fold — MAX_LEN 4/6, #[kani::unwind(5/7)] (diff macro lines 52–69).
• filter.rs next_chunk_dropless — MAX_LEN = 6, #[kani::unwind(7)] (lines 319–338).
• filter_map.rs next_chunk — MAX_LEN = 5, #[kani::unwind(6)] (lines 377–396).
• take.rs spec_fold / spec_for_each — MAX_LEN = 5, #[kani::unwind(6)] (lines 730–757).
• zip.rs next / nth / next_back / fold / spec_fold — MAX_LEN 16/5, #[kani::unwind(6)] (lines 816–899).
• copied.rs spec_next_chunk — MAX_LEN = 16 (lines 191–207).

The authors are honest about this ("Bounded MAX_LEN because the methods iterate", diff line ~815; take.rs line ~729), which is appreciated — but honesty does not satisfy the criterion. This is the standard loop_contracts/kani::unwind-with-termination gap; the challenge explicitly requires arbitrary length, so these need loop contracts (or another accepted unbounded encoding), not finite unrolling. (Copilot raised the same point at zip.rs:744.)

Note also the enumerate.rs doc comment (diff lines ~227–230) claiming any_slice "is what makes the proof unbounded". That is inaccurate — the slice length is symbolic but capped at MAX_LEN. For the non-iterating ZST/u8 accessor proofs with MAX_LEN = isize::MAX/u32::MAX this is arguably effectively unbounded, but the char/tuple variants at MAX_LEN = 50 are plainly bounded. Please soften/correct that comment.

Blocker 2 — "The verification must hold for generic type T (no monomorphization)."

Every harness is monomorphized over a fixed menu of representative types ((), u8, char, (char, u8), and paired types for zip). No harness is generic. I recognize Kani fundamentally requires concrete entry types, so full genericity may be infeasible, and representative-type coverage is the usual pragmatic compromise. But the criterion is stated explicitly, so this should at minimum be called out and justified in the PR, and the type menu is thin for some obligations (see below).

Non-blocking soundness/coverage notes

1. get_unchecked (zip.rs) is only reached transitively. The zip harnesses call __iterator_get_unchecked, which reaches ZipImpl::get_unchecked only on a freshly built Zip at index == 0, so the self.index + idx accumulated-state path is never exercised. The challenge lists get_unchecked as a separate target; add a direct proof over arbitrary valid Zip state (index > 0). (Copilot zip.rs:730.)
2. MAY_HAVE_SIDE_EFFECT = false branches are compiled out. All zip/skip harnesses wrap slice::Iter, so the specialized nth/next_back (zip) and the idx == 0 prefix-advance branch (skip.rs:182–185) with side-effecting sources are never verified. Add a TrustedRandomAccess source with MAY_HAVE_SIDE_EFFECT = true. (Copilot zip.rs:718, skip.rs:318.)
3. map_windows drop-safety path not exercised. any_buffer only instantiates Copy, trivial-drop types, so push's "update start before drop_in_place" panic-safety reasoning and non-trivial drop glue are never covered. Add a drop-requiring (ideally panicking-drop) type. (Copilot map_windows.rs:368.)
4. filter_map output type pinned to usize. needs_drop::<B>() is always false, so the Guard::drop path the comment claims to cover is compiled out. Parameterize the mapped output type. (Copilot filter_map.rs:254.)
5. N = 0 chunk case omitted for filter/filter_map next_chunk*. Worth adding for completeness (Copilot filter.rs:253, filter_map.rs:249).

Bottom line

Sound, non-vacuous, well-documented harnesses covering (nominally) all listed functions — but the challenge's two explicit gate criteria (unbounded + generic) are not met, and get_unchecked/side-effecting/drop paths are under-covered. Requesting changes primarily on the unbounded criterion (achievable via loop contracts) and the missing direct get_unchecked proof; the monomorphization criterion should at least be explicitly justified.