Compositional Reasoning about Advanced Iterator Patterns in Rust
summary
Methodology specifies and verifies Rust iterator chains that include closures with side effects, claiming precise modular reasoning about composition and captured-state updates. It implements the approach in the SMT-based pry verifier and combines inductive two-state invariants, higher-order closure call-descriptions, separation-logic-style ownership, and type-dependent contracts that attach extern specs to std iterator types. The implementation verifies map/filter/repeat patterns, integrates without client changes, reports modest annotation overhead, and leaves some adapters like mutable-in-place iteration unsupported for now.
AI-written summary · about
chapters (10)
- 0:00Iterator verification in Rust
- 1:07Hidden complexity in iterators
- 3:38Specifying iterator behavior
- 8:12Basic iterator specs
- 10:24Verifying closures in chains
- 13:33Specifying map adapter
- 16:32Incremental verification
- 19:26Realistic Rust integration
- 21:12Related work and future
- 22:22Q&A
related talks
20mModular Specification and Verification of Closures in Rust
41mFunctional Rust - An Exploration
33mRust and Haskell, sitting in a tree
15mModular Specification and Verification of Closures in Rust
14mA Refinement Methodology for Distributed Programs in Rust
28mWriting Idiomatic Libraries in Rust
58mRust for The Curious C++ Developers
19mRavencheck: Effectively-Propositional Reasoning for Rust