spec functions vs. proof functions

Now that we’ve seen both spec functions and proof functions, let’s take a longer look at the differences between them. We can summarize the differences in the following table (including exec functions in the table for reference):

As described in the spec functions section, spec functions make their bodies visible to other functions in their module and may optionally make their bodies visible to other modules as well. spec functions can also omit their bodies entirely:

spec fn f(i: int) -> int;

Such an uninterpreted function can be useful in libraries that define an abstract, uninterpreted function along with trusted axioms about the function.

Determinism

spec functions are deterministic: given the same arguments, they always return the same result. Code can take advantage of this determinism even when a function’s body is not visible. For example, the assertion x1 == x2 succeeds in the code below, because both x1 and x2 equal s(10), and s(10) always produces the same result, because s is a spec function:

mod M1 {
    use builtin::*;

    pub closed spec fn s(i: int) -> int {
        i + 1
    }

    pub proof fn p(i: int) -> int {
        i + 1
    }
}

mod M2 {
    use builtin::*;
    use crate::M1::*;

    proof fn test_determinism() {
        let s1 = s(10);
        let s2 = s(10);
        assert(s1 == s2); // succeeds

        let p1 = p(10);
        let p2 = p(10);
        assert(p1 == p2); // FAILS
    }
}

By contrast, the proof function p is, in principle, allowed to return different results each time it is called, so the assertion p1 == p2 fails. (Nondeterminism is common for exec functions that perform input-output operations or work with random numbers. In practice, it would be unusual for a proof function to behave nondeterministically, but it is allowed.)

recommends

exec functions and proof functions can have requires and ensures clauses. By contrast, spec functions cannot have requires and ensures clauses. This is similar to the way Boogie works, but differs from other systems like Dafny and F*. The reason for disallowing requires and ensures is to keep Verus’s specification language close to the SMT solver’s mathematical language in order to use the SMT solver as efficiently as possible (see the Verus Overview).

Nevertheless, it’s sometimes useful to have some sort of preconditions on spec functions to help catch mistakes in specifications early or to catch accidental misuses of spec functions. Therefore, spec functions may contain recommends clauses that are similar to requires clauses, but represent just lightweight recommendations rather than hard requirements. For example, for the following function, callers are under no obligation to obey the i > 0 recommendation:

spec fn f(i: nat) -> nat
    recommends
        i > 0,
{
    (i - 1) as nat
}

proof fn test1() {
    assert(f(0) == f(0));  // succeeds
}

It’s perfectly legal for test1 to call f(0), and no error or warning will be generated for g (in fact, Verus will not check the recommendation at all). However, if there’s a verification error in a function, Verus will automatically rerun the verification with recommendation checking turned on, in hopes that any recommendation failures will help diagnose the verification failure. For example, in the following:

proof fn test2() {
    assert(f(0) <= f(1)); // FAILS
}

Verus print the failed assertion as an error and then prints the failed recommendation as a note:

error: assertion failed
    |
    |     assert(f(0) <= f(1)); // FAILS
    |            ^^^^^^^^^^^^ assertion failed

note: recommendation not met
    |
    |     recommends i > 0
    |                ----- recommendation not met
...
    |     assert(f(0) <= f(1)); // FAILS
    |            ^^^^^^^^^^^^

If the note isn’t helpful, programmers are free to ignore it.

By default, Verus does not perform recommends checking on calls from spec functions:

spec fn caller1() -> nat {
    f(0)  // no note, warning, or error generated

}

However, you can write spec(checked) to request recommends checking, which will cause Verus to generate warnings for recommends violations:

spec(checked) fn caller2() -> nat {
    f(0)  // generates a warning because of "(checked)"

}

This is particularly useful for specifications that are part of the “trusted computing base” that describes the interface to external, unverified components.