Loops and invariants

The previous section developed a tail-recursive implementation of triangle:

fn tail_triangle(n: u32, idx: u32, sum: &mut u32)
    requires
        idx <= n,
        *old(sum) == triangle(idx as nat),
        triangle(n as nat) < 0x1_0000_0000,
    ensures
        *sum == triangle(n as nat),
{
    if idx < n {
        let idx = idx + 1;
        assert(*sum + idx < 0x1_0000_0000) by {
            triangle_is_monotonic(idx as nat, n as nat);
        }
        *sum = *sum + idx;
        tail_triangle(n, idx, sum);
    }
}

We can rewrite this as a while loop as follows:

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,
    {
        idx = idx + 1;
        assert(sum + idx < 0x1_0000_0000) by {
            triangle_is_monotonic(idx as nat, n as nat);
        }
        sum = sum + idx;
    }
    sum
}

The loop is quite similar to the tail-recursive implementation. (In fact, internally, Verus verifies the loop as if it were its own function, separate from the enclosing loop_triangle function.) Where the tail-recursive function had preconditions, the loop has loop invariants that describe what must be true before and after each iteration of the loop. For example, if n = 10, then the loop invariant must be true 11 times: before each of the 10 iterations, and after the final iteration.

Notice that the invariant idx <= n allows for the possibility that idx == n, since this will be the case after the final iteration. If we tried to write the invariant as idx < n, then Verus would fail to prove that the invariant is maintained after the final iteration.

After the loop exits, Verus knows that idx <= n (because of the loop invariant) and it knows that the loop condition idx < n must have been false (otherwise, the loop would have continued). Putting these together allows Verus to prove that idx == n after exiting the loop. Since we also have the invariant sum == triangle(idx as nat), Verus can then substitute n for idx to conclude sum == triangle(n as nat), which proves the postcondition of loop_triangle.

Just as verifying functions requires some programmer effort to write appropriate preconditions and postconditions, verifying loops requires programmer effort to write loop invariants. The loop invariants have to be neither too weak (invariant true is usually too weak) nor too strong (invariant false is too strong), so that:

• the invariants hold upon the initial entry to the loop (e.g. idx <= n holds for the initial value idx = 0, since 0 <= n)
• the invariant still holds at the end of the loop body, so that the invariant is maintained across loop iterations
• the invariant is strong enough to prove the properties we want to know after the loop exits (e.g. to prove loop_triangle’s postcondition)

As mentioned above, Verus verifies the loop separately from the function that contains the loop (e.g. separately from loop_triangle). This means that the loop does not automatically inherit preconditions like triangle(n as nat) < 0x1_0000_0000 from the surrounding function — if the loop relies on these preconditions, they must be listed explicitly in the loop invariants. (The reason for this is to improve the efficiency of the SMT solving for large functions with large while loops; verification runs faster if Verus breaks the surrounding function and the loops into separate pieces and verifies them modularly.)

Verus does allow you to opt-out of this behavior, meaning that your loops will inherit information from the surrounding context. This will simplify your loop invariants, but verification time may increase for medium-to-large functions. To opt-out for a single function or while loop, you can add the attribute #[verifier::loop_isolation(false)]. You can also opt-out at the module or crate level, by adding the #![verifier::loop_isolation(false)] attribute to the module or the root of the crate. You can then override the global setting locally by adding #[verifier::loop_isolation(true)] on individual functions or loops.