For Loops

The previous section introduced a while loop implementation of triangle:

fn loop_triangle(n: u32) -> (sum: u32)
    requires
        triangle(n as nat) < 0x1_0000_0000,
    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) < 0x1_0000_0000,
        decreases n - idx,
    {
        idx = idx + 1;
        assert(sum + idx < 0x1_0000_0000) 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) < 0x1_0000_0000,
    ensures
        sum == triangle(n as nat),
{
    let mut sum: u32 = 0;

    for idx in iter: 0..n
        invariant
            sum == triangle(idx as nat),
            triangle(n as nat) < 0x1_0000_0000,
    {
        assert(sum + idx + 1 < 0x1_0000_0000) 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.

In addition, iter.start, iter.cur, iter.end reveal the start, current, and end for the iterator of range 0..n. iter@ records all the elements that the iterator has iterated so far. In the above example, if idx=3, iter@ =~= seq![0,1,2]