Closures

In the previous chapter, we saw how to pass functions as values, which we did by referencing function items by name. However, it is more common in Rust to creating functions using closures.

Preconditions and postconditions on a closure

Verus allows you to specify requires and ensures on a closure just like you can for any other function. Here’s an example, calling the vec_map function we defined in the previous chapter:

fn test_vec_map_with_closure() {
    let double = |x: u8| -> (res: u8)
        requires 0 <= x < 128
        ensures res == 2 * x
    {
        2 * x
    };

    assert(forall |x| 0 <= x < 128 ==> call_requires(double, (x,)));
    assert(forall |x, y| call_ensures(double, (x,), y) ==> y == 2 * x);

    let mut v = Vec::new();
    v.push(0);
    v.push(10);
    v.push(20);
    let w = vec_map(&v, double);
    assert(w[2] == 40);
}

Closure capturing

One of the most challenging aspects of closures, in general, is that closures can capture variables from the surrounding context. Rust resolves this challenge through its hierarcy of function traits: FnOnce, FnMut, and Fn. The declaration of the closure and the details of its context capture determine which traits it has. In turn, the traits determine what capabilities the caller has: Can they call it more than once? Can they call it in parallel?

See the Rust documentation for a more detailed introduction.

In brief, the traits provide the following capabilities to callers and restrictions on the context capture:

Verus does not yet support borrowing mutably from the context, though it does handle moving and immutable borrows easily. Therefore, Verus has better support for Fn and FnOnce—it does not yet take advantage of the capturing capabilities supported by Rust’s FnMut.

Fortunately, both move-captures and immutable-reference-captures are easy to handle, as we can simply take their values inside the closure to be whatever they are at the program point of the closure expression.

Example:

fn example_closure_capture() {
    let x: u8 = 20;

    let f = || {
        // Inside the closure, we have seamless access to
        // variables defined outside the closure.
        assert(x == 20);
        x
    };
}