Verify safety of iterator adapter functions (Challenge 16)

[kasimte]

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

71 Kani harnesses cover the safe and unsafe methods across 13 iterator adapter files in library/core/src/iter/adapters/. main has no harnesses for these adapters, so this PR adds them. Each method's safety precondition is the existing upstream contract; every harness states the precondition and enforces it with a mirrored kani::assume (see Safety contracts for why #[requires] attributes are not used at this pin).

Verified at toolchain nightly-2026-09-25, Kani pin 1640445, CBMC 6.11.

Unbounded length and generic T are not literally met. This is a committee question open across the sentence-pair challenges (#681).

Requirements checklist

Requirement	Status	Notes
The 10 named unsafe functions	8 of 10	Per-function harnesses verify each is UB-free under its precondition. The nightly-2026-09-25 subtree update (#687) deleted the clone.rs and map.rs next_unchecked impls; those two methods are now the contracted UncheckedIterator::next_unchecked trait default, with no adapter-specific code left to prove.
The 17 safe abstractions	Done	37 harnesses. 15 have dedicated harnesses; array_chunks::next_back_remainder and zip::nth have none, and each one's unsafe internal is covered transitively (via fold and next respectively — see Known limitations).
Unbounded (arbitrary-length slices)	Partial. See Known limitations	Reached via loop contracts and arbitrary-state proofs where the structure allows; the rest stay bounded at documented tool or structural walls.
Generic type T	Pragmatic	Concrete type menu covers the behavioral axes (see Known limitations).
Absence of UB	Done, with two tool-scope residuals	Mapped per Kani check class against the four listed UBs. Dangling or misaligned pointers fall to CBMC's pointer_dereference class. Invalid values are checked where raw bytes become typed. Uninitialized reads have no check class at the repo's CI flags, because Kani's uninit checking is opt-in and not in run-kani.sh. Mutating immutable bytes has no Kani check class, a repo-wide tool limitation.
Safety contracts	Enforced via kani::assume	Each precondition is stated as a comment and enforced by a kani::assume in its harness, paired with a kani::cover non-vacuity witness. These __iterator_get_unchecked methods are trait-impls on generic adapters; proof_for_contract cannot resolve their qualified paths at this pin (kani#4084; kani#1997 added only partial trait-method support), so they cannot be proven as contracts, and the autoharness pass exits non-zero when a #[requires] is attached to them — hence the comment form. StepBy::original_step is inherent, so it carries a real checked #[ensures] via proof_for_contract.

Known limitations

• Input-domain bounds (two-tier). Harnesses with functional-equality assertions are bounded. The assertion's value reads force CBMC to bit-blast the backing array. The asserted u8 variant runs at 256; the verified property is slice-length-independent, so a 256-element witness is adequate. Assertion-free UB companions verify the same unchecked accesses at a large cap (100_000 for u8; isize::MAX for ZSTs). Slice length is fully symbolic within each bound.
• array_chunks::next_back_remainder (tool wall). Has no dedicated harness: goto-instrument --dfcc hangs for hours instrumenting the next_chunk/IntoIter/MaybeUninit machinery under -Z loop-contracts, and --harness-timeout does not cover that stage (kani#4967; a related failure-isolation gap is kani#4966). Its unsafe internal (unwrap_err_unchecked, reached through __iterator_get_unchecked) is covered by the array_chunks::fold harness.
• zip::fold / zip::nth (tool wall). fold is verified at a fixed concrete length rather than unbounded, and nth has no dedicated harness. The sound unbounded encoding is a loop contract whose invariant re-establishes the slice-cursor validity the loop havoc discards; that fix is filed but unmerged (PR kani#4957, issue kani#4911), and is additionally blocked by method-calls-in-loop_invariant mis-lowering (kani#4796). nth's only live get_unchecked (via super_nth → next) is already covered by check_zip_next_u8.
• Chunk-harness scope. The filter/filter_map chunk harnesses cover N >= 1. The SAFETY argument for the unchecked write is that idx < N whenever the closure runs, which requires N >= 1.
• zip::spec_fold (tool wall). Its only sound loop invariant is the TrustedLen exactness relation, which needs a size_hint call. Method calls inside kani::loop_invariant mis-lower at the pinned Kani (kani#4796), so the loop cannot carry a source-level contract. Verified by a bounded end-to-end harness.
• filter/filter_map chunk functions (structural). The traversal loop lives in the generic Iterator::try_for_each default, behind a capturing closure, so no adapter-level loop contract can attach. Contracting the shared default would route every std proof through the loop-contract transform (kani#4893). Verified by bounded end-to-end harnesses.
• Generic type T. Kani needs concrete types, because CBMC operates on concrete GOTO programs, so a single generic proof is not possible with this tool. The unsafe operations depend on size_of, align_of, and drop glue, not on type identity, and the type menu covers those axes: u8, () for a ZST, char for the validity niche, (char, u8) for padding, and Clone types with real drop glue including a panicking destructor. Deferred to the committee (Challenge 25: Verify the safety of VecDeque (unbounded, symbolic ring layouts, contracts on all 13 unsafe fns) #681).

Source code modifications

Three loop-contract invariants via #[cfg_attr(kani, kani::loop_invariant(...))], all verified inductive (base and step), plus one explicit assigns clause:

• take.rs spec_fold and spec_for_each: kani::index <= end
• array_chunks.rs fold: i <= inner_len, with kani::loop_modifies(&i, &accum) supplying the assigns clause CBMC cannot infer

Non-Kani builds are unaffected.

Contract changes versus main: the upstream #[requires] on the unsafe methods are removed (see Safety contracts above — documentation-only at this pin, enforced by the mirrored kani::assume instead). Skip::__iterator_get_unchecked's precondition is kept in overflow-safe subtraction form (as a comment). StepBy::original_step keeps one added checked #[ensures].

Upstream Kani contributions

We authored kani#4865 and kani#4916 toward resolving trait-impl and fn-pointer contract targets; both are merged and in this pin, but do not yet reach the generic-adapter __iterator_get_unchecked shape here (kani#4084). The unbounded zip::fold/nth encoding needs a separate fix, filed as PR kani#4957 (unmerged, issue kani#4911).

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 - 71 successfully verified harnesses, 0 failures, 71 total. Each assume-bearing harness also reports ** 1 of 1 cover properties satisfied.

Verification techniques

1. Two-tier symbolic arrays (any_slice_of_array). Asserted harnesses run at 256 for u8, where the assertion forces array bit-blasting. Assertion-free UB companions run at 100_000 for u8 and isize::MAX for ZSTs. Length is fully symbolic within each bound.
2. Loop contracts. Real inductive invariants on the annotated loops in take.rs and array_chunks.rs, which Kani abstracts without per-harness unwind bounds.
3. Arbitrary-state proofs of the real functions. Zip::get_unchecked runs over its full valid state, with index havoced over 0..=len. map_windows's Buffer runs with start havoced over its full invariant range, which is every state reachable after any number of pushes, and therefore any source length. Both run for a Copy type and a drop-glue type.
4. Drop glue. Clone types with real destructors, including one that panics on drop, exercise the Buffer and clone drop paths a Copy element type skips. The panic path is verified UB-free (its array::write fill loop is capped by #[kani::unwind(5)], whose unwinding assertion confirms the cap is complete).
5. Checked contract where resolvable. StepBy::original_step is inherent, so it carries #[ensures] checked by #[kani::proof_for_contract].
6. Non-vacuity witnesses. Every assume-bearing harness carries a kani::cover (42 harnesses, none uncovered).

Unsafe functions (8 of 10 named)

Function	File	Harnesses
__iterator_get_unchecked	cloned.rs	6 (u8, unit, char, tup, drop-glue type, u8@u32::MAX companion)
next_unchecked	cloned.rs	removed by the #687 subtree update (now the contracted UncheckedIterator::next_unchecked default)
__iterator_get_unchecked	copied.rs	5 (u8, unit, char, tup, u8@u32::MAX companion)
__iterator_get_unchecked	enumerate.rs	5 (u8, unit, char, tup, u8@u32::MAX companion)
__iterator_get_unchecked	fuse.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	map.rs	5 (u8, unit, char, tup, u8@u32::MAX companion)
next_unchecked	map.rs	removed by the #687 subtree update (same)
__iterator_get_unchecked	skip.rs	4 (u8, unit, char, tup)
__iterator_get_unchecked	zip.rs	4 (u8, unit, char, tup)
get_unchecked	zip.rs	1 direct (arbitrary index <= len state, functional asserts), plus transitive via next, next_back, and fold

Safe abstractions (17)

Function	File	Harnesses
next_back_remainder	array_chunks.rs	0 direct — dropped at a tool wall (kani#4967); unwrap_err_unchecked path covered via fold
fold	array_chunks.rs	1 (N=2 u8, arbitrary-length via source-level loop contract, no unwind bound)
spec_next_chunk	copied.rs	4 (N=2/3 u8, N=2 unit/char)
next_chunk_dropless	filter.rs	3 (bounded e2e, structural wall documented in-code)
next_chunk	filter_map.rs	3 (bounded e2e, structural wall documented in-code)
as_array_ref	map_windows.rs	9 shared (N=2/3 u8, clone N=2, clone-before-next N=2, N=2 u32, N=2 drop-glue type, N=2 panicking-drop should_panic, 2 arbitrary-state: u8 and drop-glue)
as_uninit_array_mut	map_windows.rs	same 9 (exercised via Buffer::clone and directly in the arbitrary-state harness)
push	map_windows.rs	same 9 (includes arbitrary-state proofs over the full start <= N invariant range: both push branches at every reachable offset, with post-state effect assertions that start advances or wraps and the pushed element lands at the window's back)
drop	map_windows.rs	same 9 (includes a destructor that panics, verified to unwind without UB, and drop from arbitrary post-push state)
original_step	step_by.rs	4 (size_hint u8/char, next u8, next_back u8), plus 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	1 (u8; fixed concrete length — see Known limitations)
next	zip.rs	3 (u8, char, and a side-effecting Map source)
nth	zip.rs	0 direct — no dedicated harness; covered via next (see Known limitations)
next_back	zip.rs	1 (u8)
spec_fold	zip.rs	1 (bounded e2e, tool wall documented in-code)

Test plan

• Full 71-harness suite verified locally at the tool_config pin (Kani 0.68.0, CBMC 6.11.0) with the CI flag set: 71/71.
• CI green on this head: all required jobs pass — build, both upstream_test, the four verify-std partitions, and both autoharness runs. The only non-passing checks are the non-required Kani Metrics jobs (macOS fails, ubuntu cancelled), which do not gate the PR; the macOS failure reproduces on main's own metrics run.

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.

[kasimte]

The latest commits extend the harness coverage in three ways:

• Input length: assertion-free UB-coverage companions verify the u8 accessor paths at u32::MAX input length. The functional-equality variants keep their bounds: their assertion forces CBMC to bit-blast the array, which succeeds at 5000 elements but fails with "array too large for flattening" at u32::MAX. The reason for each split is documented in-code.
• Type menu: Clone types with real drop glue on map_windows and cloned, including a destructor that panics, with the panic path verified UB-free.
• State space: a direct proof of Zip's get_unchecked over arbitrary index <= len states (with functional asserts), plus a MAY_HAVE_SIDE_EFFECT = true source variant.

[kasimte]

Pushed 9a8654f: every kani::assume in these harnesses is now paired with a kani::cover witness that the restricted input set is non-empty — 55 harnesses across 11 adapter modules (the remaining harnesses constrain no inputs). Cover properties appear in each verification run's report; the CI logs at this head show all 55 reporting SATISFIED. Full suite green.

[feliperodri]

Thanks @kasimte. Reviewed against all three open Challenge 16 solutions (#549/#602/#632) with our vacuity tooling + local Kani (pinned Kani 0.67.0 / CBMC 6.8.0). Of the three, we're prioritizing this one — it's the soundest: the earlier loop_invariant(true) issue (T2b) is fully resolved (0 occurrences; the 5 invariants are now real inductive bounds like kani::index <= end / self.index <= len), no cfg(kani) body swaps, no assume-the-conclusion, symbolic inputs, and a representative local run passed (step_by original_step proof_for_contract, cloned get_unchecked, zip nth, take spec_fold, zip spec_fold_unbounded — all VERIFICATION SUCCESSFUL).

Requesting changes because it does not yet meet the challenge's stated success criteria:

1. Generic-T not met (hard requirement). Every harness is monomorphized to concrete element types (u8/char/unit/tuple/DropToken). The challenge requires the proofs to hold for generic T with no monomorphization.
2. Unbounded not met for several targets. array_chunks::fold, filter::next_chunk_dropless, filter_map::next_chunk, zip::spec_fold are unwind-capped (unwind(9), MAX_LEN≈8), map_windows is exercised with only 2 next() calls, and zip::get_unchecked is bounded to MAX_LEN=64. The challenge requires arbitrary length.
3. The three *_unbounded harnesses re-implement the loop body (hand-written inductive fragments doing get_unchecked_mut/copy_nonoverlapping) rather than proving the real function — so they don't actually verify the shipping code's unbounded behavior.
4. Contracts largely unproven as contracts. Only step_by::original_step has a #[kani::proof_for_contract]; the other ~10 #[requires] are mirrored via kani::assume in plain proofs (understood given Kani can't target trait-impl methods, but the criterion says "write and prove the contract").

To be accepted this needs generic-T proofs (or a documented, committee-accepted rationale for the Kani limitation) and genuinely unbounded proofs of the real functions. Great progress — this is the front-runner.

[kasimte]

Thanks for the detailed review. Head b756a507 (which also merges current main, resolving the conflict) responds to each item. Statuses are per-item, since two of them end at tool or structural walls rather than fixes.

1. Generic-T: monomorphization is architectural in Kani, so this takes the path the review offered. The behavioral-class menu and parametricity argument are documented in the body, and we would welcome the committee adjudicating that rationale. For calibration, the newer sibling challenges carry an explicit waiver with this meaning: "For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only" (0026-rc, 0029-boxed). Challenge 16 predates that convention.
2. Unbounded: two of the six named targets are now genuinely unbounded, one is re-encoded, and three end at documented walls. array_chunks::fold carries a source-level loop contract on the real loop (inductive invariant plus explicit kani::loop_modifies), with no unwind cap and symbolic backing; getting there crossed CBMC aborts with l2_rename_rvalues case struct' not handled` when a zero-sized closure is a loop_modifies target kani#4786, the zero-sized loop_modifies-target crash, fixed upstream in Skip ZST targets in loop_modifies assigns clause kani#4792 after this repo's pin, so the harness uses a scalar accumulator. map_windows is re-proven from arbitrary Buffer state, with start havoced over the struct's documented invariant range, which covers every reachable state and hence any number of prior pushes. zip::get_unchecked is raised from 64 to the 5000 tier the sibling harnesses use (a bound-parity fix, not an unbounded proof). zip::spec_fold and the filter pair remain bounded, with the exact mechanism documented in-code: spec_fold's only sound invariant needs a size_hint call, and method calls in loop_invariant mis-lower at the pinned Kani ("not enough arguments, inserting non-deterministic value", filed as #[kani::loop_invariant] with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796); the filter pair's traversal loop lives in the generic try_for_each default behind a capturing closure, out of reach of an adapter-level contract.
3. The three *_unbounded re-implementations are deleted; the real-function proofs and documented walls above replace them.
4. Each assume-mirrored #[requires] now cites Resolve trait methods for stubs and function contracts kani#1997 at the site; original_step's proof_for_contract is unchanged.
   Full suite re-verified locally at the pinned Kani 0.67.0 / CBMC 6.10.0: 83/83 green.
   CI note: the ubuntu verification legs (all four verify-std partitions + autoharness) are green on this head; the macOS jobs currently fail during Homebrew setup, before any verification runs (Fix macOS CI: trust diffblue/cbmc tap for Homebrew 6.0+ kani#4785).