Iterator Specifications for a Custom Type

These will be available starting May 8th

To reason about iteration over your own custom type, you need to:

1. Define the iterator struct, similar to how various Rust types have a corresponding iterator type; e.g., a Rust slice relies on a std::slice::Iter struct.
2. Implement the standard Rust Iterator trait (next).
3. Implement the IteratorSpecImpl trait to provide Verus specification.
4. Write a constructor function for your type and annotate it with #[verifier::when_used_as_spec(...)].

To illustrate this process, in the example below, we’ll imagine that Vec doesn’t provide an iterator, so we’re going to implement one for it.

NOTE At present, Verus only supports reasoning about iterators that eventually return None, and after that point, continue to return None. We hope to eventually expand our specifications to support iterators beyond this subset.

1. The iterator struct

VecIterator holds a reference to the underlying Vec plus indices i and j marking the current and end positions. The type invariant enforces that i <= j <= v.len() at all times.

pub struct VecIterator<'a, T> {
    v: &'a Vec<T>,
    i: usize,
    j: usize,
}

impl <'a, T> VecIterator<'a, T> {
    pub closed spec fn new(v: &'a Vec<T>) -> Self {
        VecIterator { v, i: 0, j: v.len() }
    }

    pub closed spec fn elts(self) -> Seq<T> {
        self.v@
    }

    #[verifier::type_invariant]
    pub closed spec fn vec_iterator_type_inv(self) -> bool {
        &&& self.i <= self.j <= self.v.len()
        &&& self.i <= self.j <= self.v@.len()
    }
}

2. The next method

This is an ordinary Rust Iterator implementation with no Verus-specific annotations. It uses the type invariant to prove that it meets the Verus specification for next().

impl<'a, T> Iterator for VecIterator<'a, T> {
    type Item = &'a T;

    fn next(&mut self) -> (ret: Option<Self::Item>) 
    {
        proof { use_type_invariant(&*self); }
        if self.i < self.j {
            let i = self.i;
            self.i = self.i + 1;
            return Some(&self.v[i]);
        } else {
            return None;
        }
    }
}

3. The spec implementation

In vstd, Verus provides IteratorSpec, an extension of the Rust Iterator 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” for more details). Here’s a brief summary of the specification functions, with a focus on how we define them for our custom iterator.

• obeys_prophetic_iter_laws — return true to assert that this iterator satisfies the Verus specification for next. Most iterator implementations should return true here, and most iterator adaptors should return their inner iterator’s value. By returning true, we’re saying that the iterator will eventually return None, and after that point, continue to return None.
• remaining — a prophetic spec function returning the sequence of items that the iterator will eventually produce. For VecIterator, this is the subrange v[i..j].
• will_return_none — return true if the iterator will eventually return None. Infinite iterators or iterators driven by a non-terminating closure may return false.
• decrease — a termination metric for Verus’s decreases checker. By default, for loops expect this to return Some(n) where n decreases on every call to next. Here j - i works.
• initial_value_relation — a prophetic invariant relating the iterator’s initial state to the exec expression used to initialize it. This is what lets loop invariants refer to the original collection (e.g., iter.seq() == v@).
• peek — optionally returns the item at a given look-ahead index. Providing this helps Verus reason about the current element in the iteration.

impl<'a, T> IteratorSpecImpl for VecIterator<'a, T> {

    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
        true
    }

    closed spec fn remaining(&self) -> Seq<Self::Item> {
        self.v@.subrange(self.i as int, self.j as int).map(|i, v| &v)
    }

    closed spec fn will_return_none(&self) -> bool {
        true
    }

    closed spec fn decrease(&self) -> Option<nat> {
        Some((self.j - self.i) as nat)
    }
    
    #[verifier::prophetic]
    open spec fn initial_value_relation(&self, init: &Self) -> bool {
        &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
        &&& self.elts() == IteratorSpec::remaining(self).unref()
        &&& init.elts() == self.elts()
    }

    open spec fn peek(&self, index: int) -> Option<Self::Item> {
        if 0 <= index < self.elts().len() {
            Some(&self.elts()[index])
        } else {
            None
        }
    }
}

4. The constructor

Most iterator types will need to be constructed from some other type. In our example, our constructor vec_iter will take in a &'a Vec<T> and return a VecIterator<'a, T>. To enable reasoning within a for loop about the connection between the iterator and the values it was constructed from (in this case, the elements of the Vec<T>), it helps to use the #[verifier::when_used_as_spec(vec_iter_spec)] attribute, which connects the executable constructor to a spec equivalent (vec_iter_spec). This is how Verus knows the initial value of the iterator — and therefore what iter.seq() equals — at the start of the loop.

You’ll also typically want (at least) the three postconditions shown below; the first one connects the physical iterator to the spec iterator; the second enables a for loop to automatically prove termination; and the third connects the value used to construct the iterator to its prophecied sequence of yielded values.

pub open spec fn vec_iter_spec<'a, T>(v: &'a Vec<T>) -> VecIterator<'a, T> {
    VecIterator::new(v)
}

pub broadcast proof fn vec_iter_spec_properties<'a, T>(v: &'a Vec<T>)
    ensures
        #[trigger] vec_iter_spec(v).elts() == v@,
{
}

#[verifier::when_used_as_spec(vec_iter_spec)]
pub fn vec_iter<'a, T>(v: &'a Vec<T>) -> (iter: VecIterator<'a, T>)
    ensures 
        iter == vec_iter_spec(v),
        IteratorSpec::decrease(&iter) is Some,
        IteratorSpec::initial_value_relation(&iter, &vec_iter_spec(v)),
{
    let i = VecIterator { v: v, i: 0, j: v.len() };
    assert(i.elts() == IteratorSpec::remaining(&i).unref());     // OBSERVE
    i
}

5. Implementing DoubleEndedIterator

If your iterator supports backward traversal, implement the standard Rust DoubleEndedIterator trait, which adds a next_back method:

impl<'a, T> DoubleEndedIterator for VecIterator<'a, T> {
    fn next_back(&mut self) -> (ret: Option<Self::Item>) {
        proof { use_type_invariant(&*self); }
        if self.i < self.j {
            self.j = self.j - 1;
            return Some(&self.v[self.j]);
        } else {
            return None;
        }
    }
}

To allow reasoning about .rev(), you also need to implement DoubleEndedIteratorSpecImpl (analogous to IteratorSpecImpl), providing a peek_back function that returns the item at a given index from the back. Without it, Verus will not know what elements the reversed iterator will produce.

impl<'a, T> DoubleEndedIteratorSpecImpl for VecIterator<'a, T> {
    open spec fn peek_back(&self, index: int) -> Option<Self::Item> {
        let len = self.elts().len();
        if 0 <= index < len {
            Some(&self.elts()[len - index - 1])
        } else {
            None
        }
    }    
}