  Iteration is a programming operation that traditionally refers to visiting
the elements of a data structure in sequence. However, modern programming
systems such as Rust, Java, and C# generalise iteration far beyond the
traditional use case. They allow iterators to be parameterised with
(potentially side-effectful) closures and support 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 three 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?
  We present the first methodology for the modular specification and
verification of advanced iteration idioms with side-effectful computations. It
addresses the three challenges above using a combination of inductive two-state
invariants, higher-order closure contracts, and separation logic-like
ownership. We implement and our methodology in a state-of-the-art SMT-based
Rust verifier. Our evaluation shows that our methodology is sufficiently
expressive to handle advanced and idiomatic iteration idioms and requires
modest annotation overhead.
