Fn vs FnOnce in spec code

[utaal]

We currently only support Fn function bounds (not FnOnce or FnMut).

However in this situation:

use pervasive::map::*;

verus! {

spec fn foo_1(m1: Map<int, int>) -> Map<int, int> {
    Map::new(
        |key: int| m1.dom().contains(key),
        |key: int| m1[key],
    )
}

spec fn foo_2(m1: Map<int, int>) -> Map<int, int> {
    let kk = |key: int| m1.dom().contains(key);
    let vv = |key: int| m1[key];
    Map::new(kk, vv)
}
}

while foo_1 typechecks, foo_2 doesn't: "expected a closure that implements the Fn trait, but this closure only implements FnOnce". The error message explains that kk and vv are FnOnce because m1 is moved into them. However, Map::new expects Fn functions.

foo_1 wouldn't borrow-check in regular rust either, but we don't borrow-check spec functions. This behavior appears to be an asymmetry in how the function traits for closures are determined and how that influences the borrow-checking constraints.

In fact, one can force the closures in the lets to be Fn by ascription:

spec fn foo_1(m1: Map<int, int>) -> Map<int, int> {
    let kk: Box<dyn Fn(int) -> bool> = Box::new(|key: int| m1.dom().contains(key));
    let vv: Box<dyn Fn(int) -> int> = Box::new(|key: int| m1[key]);
    Map::new(kk, vv)
}

This again typechecks (but we currently fail because we don't support dyn).

This behavior is surprising and there may be different ways to address it.

We could change the trait bounds on Map::new to be FnOnce, which I believe would be sound (as Map::new is spec).

Initially found by @matthias-brun.

[Chris-Hawblitzel]

Interesting. From discussions about executable closures with @tjhance , it's likely we'd want to use a new type, FnSpec for spec closures, in order to reserve Fn for executable closures. Hopefully, we can use the syntax macro to coerce spec closure constructors to type FnSpec, including doing whatever is necessary to make sure that examples like the one above work correctly.

[tjhance]

I agree it ought to be sound to declare the parameter to Map::new as FnOnce (same for any other spec function). It might be confusing to the users though.

This might be relevant: a few days ago, Chris and I were discussing exec-mode function arguments and discussed the possibility of adding FnSpec.

To summarize that conversation:

• When an exec-mode function is called it might be non-terminating or non-deterministic
• Spec-functions are expected to be terminating, deterministic functions.
• Exec-mode stuff can always be cast to spec-mode, which leads to an inconsistency
• Therefore, in general, the "exec call" or a function might have different behavior than the "spec call"
• That could lead to user confusion, who might expect them to be the same

As such, we came up with a possible solution:

• Introduce the FnSpec trait, which indicates that a function is a terminating, deterministic function.
• In order to "call" a function in spec-mode, it has to be FnSpec.
  • If a function isn't FnSpec, then you can only talk about it terms of pre-conditions and post-conditions, as in the exec-function proposal.
• We port existing code to use FnSpec instead of Fn
• Using the syntax macro, we can do some trickery to make sure that user-declared closures are type-checked as FnSpec.

I think this plan would also solve the problem you bring here due to the last bullet point.

[utaal]

A variation of this (where FnSpec is a type) has been implemented.