Putting It All Together

To show how spec, proof, and exec code work together, consider the example below of computing the n-th triangular number. We’ll cover this example and the features it uses in more detail in Chapter 4, so for now, let’s focus on the high-level structure of the code.

We use a spec function triangle to mathematically define our specification using natural numbers (nat) and a recursive description. We then write a more efficient iterative implementation as the exec function loop_triangle (recall that exec is the default mode for functions). We connect the correctness of loop_triangle’s return value to our mathematical specification in loop_triangle’s ensures clause.

However, to successfully verify loop_triangle, we need a few more things. First, in executable code, we have to worry about the possibility of arithmetic overflow. To keep things simple here, we add a precondition to loop_triangle saying that the result needs to be less than one million, which means it will certainly fit into a u32.

We also need to translate the knowledge that the final triangle result fits in a u32 into the knowledge that each individual step of computing the result won’t overflow, i.e., that computing sum = sum + idx won’t overflow. We can do this by showing that triangle is monotonic; i.e., if you increase the argument to triangle, the result increases too. Showing this property requires an inductive proof. We cover inductive proofs later; the important thing here is that we can do this proof using a proof function (triangle_is_monotonic). To invoke the results of our proof in our exec implementation, we assert that the new sum fits, and as justification, we an invoke our proof with the relevant arguments. At the call site, Verus will check that the preconditions for triangle_is_monotonic hold and then assume that the postconditions hold.

Finally, our implementation uses a while loop, which means it requires some loop invariants, which we cover later.

spec fn triangle(n: nat) -> nat
    decreases n,
{
    if n == 0 {
        0
    } else {
        n + triangle((n - 1) as nat)
    }
}

proof fn triangle_is_monotonic(i: nat, j: nat)
    ensures
        i <= j ==> triangle(i) <= triangle(j),
    decreases j,
{
    // We prove the statement `i <= j ==> triangle(i) <= triangle(j)`
    // by induction on `j`.

    if j == 0 {
        // The base case (`j == 0`) is trivial since it's only
        // necessary to reason about when `i` and `j` are both 0.
        // So no proof lines are needed for this case.
    }
    else {
        // In the induction step, we can assume the statement is true
        // for `j - 1`. In Verus, we can get that fact into scope with
        // a recursive call substituting `j - 1` for `j`.

        triangle_is_monotonic(i, (j - 1) as nat);

        // Once we know it's true for `j - 1`, the rest of the proof
        // is trivial.
    }
}

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
}