Iterators

These will be available starting May 8th

Verus supports verifying for loops over any type that implements the Rust Iterator trait, as long as that type comes with appropriate Verus specifications. This page explains how to write loop invariants using the specifications Verus provides in vstd. For information on how to add specifications to your own iterator type, see Iterator Specifications for a Custom Type.

Ghost State in For Loops

Verus allows you to name the iterator that Rust uses inside a for loop:

for x in my_iter: some_expression
    invariant
        // can refer to iter.index() and iter.seq()
{
    // x is the current element; iter tracks ghost state
}

You can use this name (my_iter above) to refer to the number of iterations thus far: my_iter.index(). You can also use my_iter.seq() to refer to the complete sequence of items the iterator will yield, from its starting position. This is a prophetic value: Verus knows it up front even though the iterator hasn’t run yet. In for loops without a break, after the loop completes, we also know that my_iter.index() == my_iter.seq().len().

Example: checking all elements are positive

fn all_positive(v: &Vec<u8>) -> (b: bool)
    ensures
        b <==> (forall|i: int| 0 <= i < v.len() ==> v[i] > 0),
{
    let mut b: bool = true;

    for x in iter: vec_iter(v)
        invariant
            b <==> (forall|i: int| 0 <= i < iter.index() ==> v[i] > 0),
    {
        b = b && *x > 0;
    }
    b
}

The invariant tracks progress via iter.index(). When the loop finishes, we know the invariant held for every i up to iter.seq().len(), which equals v.len().

Range iterators

Standard Rust integer ranges work the same way:

fn build_range(n: u32) -> (v: Vec<u32>)
    ensures
        v.len() == n,
        forall|i: int| 0 <= i < n ==> v[i] == i,
{
    let mut v: Vec<u32> = Vec::new();
    for i in r_iter: 0..n
        invariant
            v.len() == r_iter.index(),
            forall|j: int| 0 <= j < v.len() ==> v[j] == r_iter.seq()[j],
    {
        v.push(i);
    }
    v
}

For a range 0..n, r_iter.seq()[k] == k, so r_iter.seq()[r_iter.index()] equals the current element i.

Omitting the wrapper

If you don’t need ghost state in your invariant, you can omit the my_iter: binding:

fn sum_multiples_of_3() -> u64 {
    let mut n: u64 = 0;
    for x in 0..10
        invariant n == x * 3,
    {
        n += 3;
    }
    assert(n == 30);
    n
}

Reversed iteration

The same specification style applies to Iterator adaptors. For example, for iterators that implement Rust’s DoubleEndedIterator, you can call .rev() to iterate in reverse. The seq() and index() specifications work identically — they refer to the reversed sequence:

fn test_reversed(v: &Vec<u8>) -> (w: Vec<u8>)
    ensures
        w@ == v@.reverse(),
{
    let mut w: Vec<u8> = Vec::new();
    for x in iter: v.iter().rev()
        invariant
            w.len() == iter.index(),
            forall|i: int| 0 <= i < w.len() ==> w@[i] == *iter.seq()[i],
    {
        w.push(*x);
    }
    w
}