Spec Closures

Verus supports anonymous functions (known as “closures” in Rust) in ghost code. For example, the following code from earlier in this chapter uses an anonymous function |i: int| 10 * i to initialize a sequence with the values 0, 10, 20, 30, 40:

proof fn test_seq2() {
    let s: Seq<int> = Seq::new(5, |i: int| 10 * i);
    assert(s.len() == 5);
    assert(s[2] == 20);
    assert(s[3] == 30);
}

The anonymous function |i: int| 10 * i has type spec_fn(int) -> int and has mode spec. Because it has mode spec, the anonymous function is subject to the same restrictions as named spec functions. (For example, it can call other spec functions but not proof functions or exec functions.)

Note that in contrast to standard executable Rust closures, where Fn, FnOnce, and FnMut are traits, spec_fn(int) -> int is a type, not a trait. Therefore, ghost code can return a spec closure directly, using a return value of type spec_fn(t1, ..., tn) -> tret, without having to use dyn or impl, as with standard executable Rust closures. For example, the spec function adder, shown below, can return an anonymous function that adds x to y:

spec fn adder(x: int) -> spec_fn(int) -> int {
    |y: int| x + y
}

proof fn test_adder() {
    let f = adder(10);
    assert(f(20) == 30);
    assert(f(60) == 70);
}