Quantifiers

Suppose that we want to specify that all the elements of a sequence are even. If the sequence has a small, fixed size, we could write a specification for every element separately:

spec fn is_even(i: int) -> bool {
    i % 2 == 0
}

proof fn test_seq_5_is_evens(s: Seq<int>)
    requires
        s.len() == 5,
        is_even(s[0]),
        is_even(s[1]),
        is_even(s[3]),
        is_even(s[3]),
        is_even(s[4]),
{
    assert(is_even(s[3]));
}

Clearly, though, this won’t scale well to larger sequences or sequences of unknown length.

We could write a recursive specification:

spec fn all_evens(s: Seq<int>) -> bool
    decreases s.len(),
{
    if s.len() == 0 {
        true
    } else {
        is_even(s.last()) && all_evens(s.drop_last())
    }
}

proof fn test_seq_recursive(s: Seq<int>)
    requires
        s.len() == 5,
        all_evens(s),
{
    assert(is_even(s[3])) by {
        reveal_with_fuel(all_evens, 2);
    }
}

However, using a recursive definition will lead to many proofs by induction, which can require a lot of programmer effort to write.

Fortunately, Verus and SMT solvers support the universal and existential quantifiers forall and exists, which we can think of as infinite conjunctions or disjunctions:

(forall|i: int| f(i)) = ... f(-2) && f(-1) && f(0) && f(1) && f(2) && ...
(exists|i: int| f(i)) = ... f(-2) || f(-1) || f(0) || f(1) || f(2) || ...

With this, it’s much more convenient to write a specification about all elements of a sequence:

proof fn test_use_forall(s: Seq<int>)
    requires
        5 <= s.len(),
        forall|i: int| 0 <= i < s.len() ==> #[trigger] is_even(s[i]),
{
    assert(is_even(s[3]));
}

Although quantifiers are very powerful, they require some care, because the SMT solver’s reasoning about quantifiers is incomplete. This isn’t a deficiency in the SMT solver’s implementation, but rather a deeper issue: it’s an undecidable problem to figure out whether a formula with quantifiers, functions, and arithmetic is valid or not, so there’s no complete algorithm that the SMT solver could implement. Instead, the SMT solver uses an incomplete strategy based on triggers, which instantiates quantifiers when expressions match trigger patterns.

This chapter will describe how to use forall and exists, how triggers work, and some related topics on choose expressions and closures.