Compositional Reasoning for Side-effectful Iterators and Iterator Adapters

TL;DR

This paper introduces a novel methodology for modularly specifying and verifying complex, side-effectful iterators and iterator chains in programming languages like Rust, addressing key challenges in reasoning about their behavior and effects.

Contribution

It presents the first comprehensive approach combining invariants, closure contracts, and ownership for verifying advanced iteration idioms with side effects.

Findings

Methodology effectively handles complex iteration idioms.

Requires modest annotation overhead.

Implemented in a Rust verifier with successful case studies.

Abstract

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.