Iteration is a control-flow mechanism that consists of repeating statements. Iterators provide an object-oriented abstraction to iteration. Simple iterators confer access to elements of a data structure, but modern languages such as Rust, Java, and C# generalise iteration far beyond this simple use case, allowing iterators to be parameterised with closures (which can modify their captured state as a side effect) and supporting the composition of iterators to form iterator chains, where each iterator in the chain consumes values from its predecessor and produces values for its successor. Such generalisations pose four major challenges for modular specification and verification of iterators and the client code using them: (1) How can parameterised iterators be specified modularly and their (accumulated) side effects reasoned about? (2) How can the behaviour of an iterator chain be derived from the specifications of its component iterators? (3) How can proofs about such iterators be automated? (4) How to integrate a concrete methodology into the standard library, without requiring the client code to change?

We present a methodology for the modular specification and verification of advanced iteration idioms with computations affecting captured state as a side effect. It addresses the four challenges above using a combination of inductive two-state invariants, higher-order closure contracts, separation logic-like ownership, and a novel type of out-of-band contracts. We implement our methodology in a state-of-the-art SMT-based Rust verifier. Our evaluation shows that our methodology is sufficiently expressive to handle advanced, idiomatic iteration patterns and requires modest annotation overhead.