# Implementing Iterator Specifications for Infinite Iterators Somewhat surprisingly, we can also follow the same [steps needed to verify an iterator implementation](iterator-specs.md) for a custom type that implements an infinite iterator! Let's start with an infinite iterator built on a counter that increments each time we call `next()`, wrapping when we would otherwise overflow. ### 1. The iterator struct `IterCtr` holds the 64-bit counter value (`count`), and a [prophetic](https://verus-lang.github.io/verus/verusdoc/vstd/proph) length field that defines how long the sequence of return values will be. At this point, we don't know what the length is; we just know it has some value. ```rust {{#include ../../../../examples/guide/iterators.rs:ctr_iter_def}} ``` ### 2. The `next` method This is an ordinary Rust `Iterator` implementation. However, we do need to include a proof that `next()` meets its obligations, especially the obligation that the value returned by `next()` matches the first element in the prophesized `remaining` sequence. Here, the key idea is to swap the existing prophecy variable (in `self.len`) with a newly created prophecy variable. We then resolve the old prophecy variable in such a way that its final value is one more than the prophecy variable we just created. This is enough to show that the prophetic sequence's length decreased by one, just as the spec for `next()` demands. ```rust {{#include ../../../../examples/guide/iterators.rs:ctr_normal_iter}} ``` ### 3. The spec implementation In `vstd`, Verus provides `IteratorSpec`, an extension of the Rust [`Iterator`](https://doc.rust-lang.org/std/iter/trait.Iterator.html) trait that defines a variety of specification functions, as well as the Verus specs for the `next()` function. To enable us to reason about our custom iterator, we need to implement the Verus-provided `IteratorSpecImpl` trait (not the `IteratorSpec` trait that defines the specs -- see ["External trait specifications"](external_trait_specifications.md) for more…