For Loops

The previous section introduced a while loop implementation of triangle:

fn loop_triangle(n: u32) -> (sum: u32)
    requires
        triangle(n as nat) <= u32::MAX,
    ensures
        sum == triangle(n as nat),
{
    let mut sum: u32 = 0;
    let mut idx: u32 = 0;
    while idx < n
        invariant
            idx <= n,
            sum == triangle(idx as nat),
            triangle(n as nat) <= u32::MAX,
        decreases n - idx,
    {
        idx = idx + 1;
        assert(sum + idx <= u32::MAX) by {
            triangle_is_monotonic(idx as nat, n as nat);
        }
        sum = sum + idx;
    }
    sum
}

We can rewrite this as a for loop as follows:

fn for_loop_triangle(n: u32) -> (sum: u32)
    requires
        triangle(n as nat) <= u32::MAX,
    ensures
        sum == triangle(n as nat),
{
    let mut sum: u32 = 0;

    for idx in 0..n
        invariant
            sum == triangle(idx as nat),
            triangle(n as nat) <= u32::MAX,
    {
        assert(sum + idx + 1 <= u32::MAX) by {
            triangle_is_monotonic((idx + 1) as nat, n as nat);
        }
        sum = sum + idx + 1;
    }
    sum
}

The only difference between this for loop and the while loop is that idx is automatically incremented by 1 at the end of the each iteration, and we no longer need the idx <= n invariant.

For more complex examples, Verus also provides ghost specifications about the iterator used in for loops, as we discuss in the next section.