Total spec closures and partial spec closures

[Chris-Hawblitzel]

There's been recent discussion on providing better support for checking preconditions on spec functions (see #764 ), with a primary goal of catching errors in specs earlier, when the spec is defined, rather than later, in the middle of using the spec to verify something more complicated. I'd like to propose extending this to higher-order specifications as well by allowing preconditions on spec closures, and having the preconditions be part of the spec closure in the style of Dafny's --> functions.

Verus supports first-class spec functions via Rust closures. For example, inside a specification, |n: int| n + 1 is a spec closure that defines a function that adds one to an integer argument n. Currently, it is possible to put preconditions (via recommends) on top-level functions (as in spec fn f(n: int) -> int recommends n != 0 { n + 1 }), but not on closures (there is nothing like |n: int| recommends n != 0 { n + 1 } yet). This proposal sketches what support for preconditions on spec closures might look like in Verus. More specifically, it proposes a new "partial" spec function type to complement the existing "total" spec function type, and proposes using Rust traits to make common library functions, such as Map::new, Seq::new, and Seq::map polymorphic over both total and partial spec function types.

Syntax (provisional)

I don't have a complete syntax in mind, but for the purposes of this proposal, I'll use the following syntax, sticking close to the current Verus syntax:

• recommends, since that's what's currently in use (but it could be called when, expects, wants, desires, ...)
• |x1: t1, ..., xn: tn| expr for total closure expressions, as in current Verus syntax
• |x1: t1, ..., xn: tn| recommends expr { expr } for partial closure expressions
• FnSpec(t1, ... tn) -> t0 for total function types, as in current Verus syntax
• FnSpec(t1, ... tn) --> t0 for partial function types, following Dafny's convention on -> and -->
• FnSpecTrait(t1, ... tn) -> t0 for the general spec function trait, implemented by both total and partial function types

Personally, I'm not attached to -> and --> and I don't like the name FnSpecTrait (FnSpec would make more sense, assuming we use something other than FnSpec for the function types, as has been proposed elsewhere).

Motivation

Verus currently checks recommends clauses on top-level spec functions. In the following example, r's call to q(n) fails q's recommends check:

spec(checked) fn q(n: int) -> int
    recommends n != 0
{
    100int / n
}

spec(checked) fn r(n: int) -> int {
    q(n) // fails recommendation check
}

One way to fix this is add a recommends to r (alternatively, as mentioned in #764 , one could suppress the check with some sort of local #[allow(...)]):

spec(checked) fn r(n: int) -> int
    recommends n != 0
{
    q(n) // ok
}

Suppose, though, that r's definition involves a closure, and the closure calls q:

spec(checked) fn r(n: int) -> int
    recommends n != 0
{
    let f = |x: int| q(x); // ???
    f(n)
}

In this case, it's not clear how the call to q(x) would satisfy q's recommends clause, since there is no x != 0 constraint on x. To motivate adding partial closure support, let's look at a few simpler alternative designs first.

1. We could simply not perform the recommends check inside a closure. However, this would miss opportunities to catch spec errors early, and could surprise and confuse programmers who expect more consistent checking.

2. We could allow programmers to add recommends clauses on closures, and then simply assume that the recommends clauses hold at the call sites to the closures without any checks. Then you could write:

spec(checked) fn r(n: int) -> int
    recommends n != 0
{
    let f = |x: int| recommends x != 0 { q(x) }; // assume x != 0 here so we can check `q(x)`
    f(n) // call f without checking recommends
}

but this would fail to catch the case where r might actually pass in a value of x = 0:

spec(checked) fn r(n: int) -> int {
    let f = |x: int| recommends x != 0 { q(x) }; // assume x != 0 here
    f(n) // call f without checking recommends; should not succeed but does
}

3. We could in some sense enforce the closure's recommends clause by implicitly replacing the body q(x) with if x != 0 { q(x) } else { arbitrary() }, so that the return value is arbitrary if the arguments don't satisfy the recommends. However, this still doesn't catch the recommends failure early, since there's still no recommends check on the call to the closure:

spec(checked) fn r(n: int) -> int {
    let f = |x: int| recommends x != 0 { q(x) }; // assume x != 0 in call to `q(x)`, but don't call `q(x)` if `x == 0`
    f(n) // succeeds, unfortunately, instead of catching recommends failure early
}

Instead, the programmer would have to discover the problem much later when they try to call r(0) and discover that it fails to obey the expected substitution rule for a function call (i.e. the call f(0) isn't equal to the body with the argument 0 substituted for the parameter x):

assert(r(0) == q(0)); // FAILS, somewhat late and mysteriously

If we want to catch recommends failures for closures early, we need to perform recommends checking on calls to the closures.

Design

Coq, F*, and Dafny all have mechanisms for attaching preconditions to specification "closures". Coq and F* attach the preconditions to the type of the closure using dependent types, which would be a major and difficult extension to Rust's type system. Dafny attaches the precondition to the closure value. This approach is much easier to integrate into Verus, so this proposal is based on this approach. Specifically, for a value v of partial function type FnSpec(t1, ... tn) --> t0, the programmer could check to see whether arguments a1, ..., an satisfy v's recommends clauses with an expression like v.recommends(a1, ..., an). (Again, I don't have a strong preference on the exact syntax here.) When a program calls v with arguments a1, ..., an, Verus would automatically insert a recommends check to make sure v.recommends(a1, ..., an) is true.

Total closures, on the other hand, would always be valid for all arguments, and would not receive a recommends check. The tradeoff is that total closures cannot make any assumptions about their arguments, so that a total closure's body is checked for recommends failures with just an assumption of true on the closure's arguments. If this leads to spurious recommends failures, then the programmer would have to suppress the failures with #[allow(...)] or switch to a partial closure. Nevertheless, total closures are still very convenient in many cases. For example, when defining a set with Set::new, it's very natural to use a total closure of type FnSpec(t) -> bool.

It should be easy to provide explicit coercions between total and partial closures (adding a recommends true when going from total to partial, or explicitly deciding to ignore the recommends when going from partial to total). However, many library functions should work seamlessly with both total and partial function types without having to use an explicit coercion. For example, Map::new and Seq::new make sense with partial closures, but are equally usable with total closures. We should be able to write Seq::new(10, |n: int| n + 1), using the total closure |n: int| n + 1, without having to explicitly coerce the total closure to a partial closure. For this, we can use a trait FnSpecTrait that is implemented by both total and partial closures:

impl<A> Seq<A> {
    /// Construct a sequence `s` of length `len` where entry `s[i]` is given by `f(i)`.
    pub spec fn new(len: nat, f: impl FnSpecTrait(int) -> A) -> Seq<A>
        recommends forall|i: int| 0 <= i < len ==> f.recommends(i)

In the case of a total closure, f.recommends(i) would be trivially satisfied.

Implementation

The implementation of total closures should be unaffected by partial closures; it would not change from the current implementation. A total closure FnSpec(t1, ..., tn) -> t0 is simply implemented as an AIR lambda of type (t1, ..., tn) -> t0.

A partial closure FnSpec(t1, ..., tn) --> t0 can be implemented as a pair of AIR lambdas (((t1, ..., tn) -> bool), ((t1, ..., tn) -> t0)), where the (t1, ..., tn) -> bool lambda holds the domain of the partial closure.

The trait FnSpecTrait(t1, ..., tn) -> t0 can dispatch to the underlying total or partial closure implementations using the existing Verus trait mechanisms based on dynamic type identifiers. (Total and partial closures would have distinct dynamic type identifiers in the AIR encoding.) There would be some extra SMT overhead in this case for things like Map::new and Seq::new compared to the current total-closure-only versions of these library functions, but I would guess it would not be a major overhead.

[utaal]

This is great.

A syntax proposal that feels a bit Rustier to me, and based on @tjhance's spec_fn/fn_spec suggestion (assuming we use when in place of recommends, as suggested in #764 (comment) ):

• fn_spec(t1, ... tn) -> t0 for total function types,
• fn_when(t1, ... tn) -> t0 for partial function types,
• FnSpec(t1, ... tn) -> t0 for the general spec function trait, implemented by both total and partial function types

[tjhance]

what about fn_total and fn_when?

[utaal]

I considered that too. I think it being a spec function is more important than it being a total function.

[Chris-Hawblitzel]

I agree; I like fn_spec because it mentions spec.

[jonhnet]

I'm delighted to hear we're moving in this direction. My recent debugging work has been frustrating in large part because of not having effective eager checks on spec fns, which has been making me contemplate on how end users will experience total spec functions: they'll find it really confusing. So I'm extremely happy to hear we're moving in a direction that supports a more consistent eager error reporting experience for partial fn constraints. Three cheers!

I also like ability to preserve the lightweight Seq::new(10, |n: int| n + 1) use case.