Loop contracts have no attach site for loops inside called iterator combinators (fold/try_for_each/collect) #4893

Requested feature: A way to apply a loop contract to a loop inside a called function —
e.g. a call-site mechanism to name a monomorphized combinator instance's loop and supply
its invariant/frame.

Use case: Verifying std functions whose iteration is expressed via iterator combinators
(fold/try_for_each/collect) for unbounded input length — e.g. Filter/FilterMap's
next_chunk and String::from_utf16{le,be}[_lossy] (verify-rust-std Challenges 16 and 10).

Link to relevant documentation:
https://model-checking.github.io/kani/reference/experimental/loop-contracts.html

Test case: see Minimal reproduction below.

Summary

kani::loop_invariant / kani::loop_modifies are written on the loop statement itself,
in the source of whatever function contains it — which works whether that function is the
harness target or a callee, as long as one can meaningfully annotate that source. When a
function's only iteration is expressed by calling an iterator combinator —
Iterator::fold, for_each, try_for_each, or collect — the loop lives in a shared
generic callee (the combinator's default body — or, for collect, the collection's
Extend impl), and the closure the caller passes contains no loop. There is no statement
in the caller to annotate, the shared body cannot carry a per-caller invariant (see
workarounds below), and there is no call-site mechanism to supply one. Such
functions currently cannot be verified for unbounded input length with
-Z loop-contracts: CBMC must unroll, and any finite #[kani::unwind(k)] bounds the
input.

This is distinct from #3599 (loop contracts on loops written inside a user closure):
there the loop is lexically present in user code; here it is in the callee, and the
user's closure contains none.

Minimal reproduction

kani combinator_wall.rs -Z loop-contracts --harness <name>:

#![feature(proc_macro_hygiene)]
#![feature(stmt_expr_attributes)]

// (1) Hand loop: kani::loop_invariant ATTACHES to the `while`. No unwind bound;
// the loop contract is size-independent, so symbolic (unbounded) `n` verifies.
#[kani::proof]
fn hand_loop_unbounded() {
    let n: u64 = kani::any();
    let mut acc: u64 = 0;
    let mut i: u64 = 0;
    #[kani::loop_invariant(i <= n && acc == i)]
    while i < n {
        acc += 1;
        i += 1;
    }
    assert!(acc == n);
}

// (2) Same computation via Iterator::fold, symbolic (unbounded) n. The loop is
// inside fold's monomorphized body; there is no statement here to annotate, and
// the closure `|acc, _| acc + 1` has no loop.
#[kani::proof]
#[kani::unwind(5)]
fn fold_symbolic_n() {
    let n: u64 = kani::any();
    let acc: u64 = (0..n).fold(0u64, |acc, _| acc + 1);
    assert!(acc == n);
}

// (3) The fold version verifies only when the INPUT is bounded (n <= 4 < unwind).
#[kani::proof]
#[kani::unwind(5)]
fn fold_bounded_pass() {
    let n: u64 = kani::any();
    kani::assume(n <= 4);
    let acc: u64 = (0..n).fold(0u64, |acc, _| acc + 1);
    assert!(acc == n);
}

Results (identical outcomes on Kani 0.67.0 and 0.68.0):

Identical computation; the only difference is while vs fold. Since n is a symbolic
u64, no finite unwind covers it — raising the unwind just moves the bound, and disabling
--unwinding-assertions would under-approximate. The failing check sits inside
Iterator::fold, not in the harness: there is no caller-side statement to carry a loop
contract. for_each and try_for_each are implemented in terms of fold/try_fold, and
collect runs the collection's FromIterator/Extend, whose iteration is likewise
inside the callee — so all of them hit the same wall.

Why the obvious workarounds don't apply

• Annotate the loop inside the generic default (e.g. Iterator::fold in core): the
  invariant needed is closure-specific — a single annotation on the shared default cannot
  express per-caller invariants — and instrumenting the default would route every
  iterator-touching proof through the loop-contract transform.
• Stub the combinator with a contracted replacement: stubbing non-overridden default
  trait methods currently fails (Stubbing non-overridden default trait methods fails with type mismatch #4588); more fundamentally, a faithful contract for
  fold would have to speak about the behavior of the passed closure, which contracts
  cannot express.
• Synthesize instead of annotate (-Z unstable-options --synthesize-loop-contracts
  — it works on the goto model, so callee loops are in scope): on this reproducer
  goto-synthesizer aborts with an internal invariant violation — Failed to synthesize a new assigns target (enumerative_loop_contracts_synthesizer.cpp:231, SIGABRT).
  Cf. goto-synthesizer crash #2927 for another long-open synthesizer crash.
• Rewrite the caller with a hand loop: works when you own the code, but for std
  functions under verification the combinator spelling is the shipping code — a
  cfg(kani) alternate body would verify something other than the shipped function.
• Note the gap is only for loops in callees: an adapter or override that contains its
  own in-body loop can be annotated normally.

The engine itself does not look like the blocker: CBMC applies loop contracts per
goto-level loop, and each monomorphized combinator instance is already a distinct goto
function — the failing check above names
<Range<u64> as Iterator>::fold::<u64, {closure@…}>. What's missing is a Kani-side way
to name such an instance's loop and supply an invariant for it, including a way to state
that invariant over the callee's locals.

Real-world instances (rust std)

• Filter/FilterMap's next_chunk traversal runs in the generic
  Iterator::try_for_each default behind a capturing closure (filter.rs,
  next_chunk_dropless: self.iter.try_for_each(|element| { … })) — no adapter-level
  attach site. Verify safety of iterator adapter functions (Challenge 16) verify-rust-std#549 documents this limitation in prose and
  has to leave those functions bounded.
• String::from_utf16be (on little-endian targets), both _lossy variants, and
  String::from_utf16le's unaligned path all end in char::decode_utf16(…).collect();
  for String the collection runs impl Extend<char> for String, i.e.
  iterator.for_each(move |c| self.push(c)) (alloc/src/string.rs). verify-rust-std's
  Challenge 10 marks these functions "(unbounded)". Contrast their sibling
  String::from_utf16, which pre-reserves and runs a hand for loop over the same
  decode_utf16 — that loop can carry a contract, so the gap is the spelling, not the
  computation. (Collecting into a growing String also reallocates, compounding with
  Support malloc and free in loops with loop contracts #3587.)

Related issues

• Loop contracts in closures and coroutines #3599 — loop contracts in closures and coroutines (user-closure loops; distinct from this)
• Support malloc and free in loops with loop contracts #3587 — malloc/free in loops with loop contracts (the reallocation facet of collect)
• Stubbing non-overridden default trait methods fails with type mismatch #4588 — stubbing non-overridden default trait methods fails (blocks the stub workaround above)
• Loop contracts in closure run too slow #4326 — loop contracts in closures run too slow

Possible directions (non-prescriptive)

• A call-site mechanism to supply an invariant/frame for a loop inside a called function
  (or loop-contract propagation into iterator combinators); or
• A documented supported pattern (pre-reserve + hand loop, as from_utf16 does) plus a
  diagnostic pointing at it when the target loop lives inside a called combinator.

Tested on Kani 0.67.0 (verify-rust-std's current pin) and 0.68.0 (latest release), macOS
aarch64; the synthesis probe used goto-synthesizer from CBMC 6.11.0. Happy to help with
reproducers or testing.