Specifying and Verifying Higher-order Rust Iterators.

In Rust, programs are often written using iterators , but these pose problems for verification: they are non-deterministic , infinite , and often higher-order , effectful and built using adapters . We present a general framework for specifying and reasoning with Rust iterators in first-order logic. Our approach is capable of addressing the challenges set out above, which we demonstrate by verifying real Rust iterators, including a higher-order, effectful Map. Using the Creusot verification platform, we evaluate our framework on clients of iterators, showing it leads to efficient verification of complex functional properties.