Loops with break

Loops can exit early using return or break. Suppose, for example, we want to remove the requirement triangle(n as nat) < 0x1_0000_0000 from the loop_triangle function, and instead check for overflow at run-time. The following version of the function uses return to return the special value 0xffff_ffff in case overflow is detected at run-time:

fn loop_triangle_return(n: u32) -> (sum: u32)
    ensures
        sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) >= 0x1_0000_0000),
{
    let mut sum: u32 = 0;
    let mut idx: u32 = 0;
    while idx < n
        invariant
            idx <= n,
            sum == triangle(idx as nat),
    {
        idx = idx + 1;
        if sum as u64 + idx as u64 >= 0x1_0000_0000 {
            proof {
                triangle_is_monotonic(idx as nat, n as nat);
            }
            return 0xffff_ffff;
        }
        sum = sum + idx;
    }
    sum
}

Another way to exit early from a loop is with a break inside the loop body. However, break complicates the specification of a loop slightly. For simple while loops without a break, Verus knows that the loop condition (e.g. idx < n) must be false after exiting the loop. If there is a break, though, the loop condition is not necessarily false after the loop, because the break might cause the loop to exit even when the loop condition is true. To deal with this, while loops with a break, as well as Rust loop expressions (loops with no condition), must explicitly specify what is true after the loop exit using ensures clauses, as shown in the following code. Furthermore, invariants that don’t hold after a break must be marked as invariant_except_break rather than invariant:

fn loop_triangle_break(n: u32) -> (sum: u32)
    ensures
        sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) >= 0x1_0000_0000),
{
    let mut sum: u32 = 0;
    let mut idx: u32 = 0;
    while idx < n
        invariant_except_break
            idx <= n,
            sum == triangle(idx as nat),
        ensures
            sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) >= 0x1_0000_0000),
    {
        idx = idx + 1;
        if sum as u64 + idx as u64 >= 0x1_0000_0000 {
            proof {
                triangle_is_monotonic(idx as nat, n as nat);
            }
            sum = 0xffff_ffff;
            break;
        }
        sum = sum + idx;
    }
    sum
}