Is there a way to pass a named spec function as a spec_fn argument?

[parno]

At present, it does not seem to be possible to pass a named spec function to a function that's expecting a spec_fn. For example, Verus yells at me when I try the obvious approach:

error[E0308]: mismatched types
   --> t.rs:120:19
    |
120 |             r.all(property_bounds_for_smallest_bitting_size)
    |               --- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `FnSpec<(int,), bool>`, found fn item
    |               |
    |               arguments to this method are incorrect
    |
    = note: expected struct `builtin::FnSpec<(builtin::int,), bool>`
              found fn item `fn(builtin::int) -> bool {property_bounds_for_smallest_bitting_size}`
note: method defined here
   --> /Users/parno/git/verus/source/vstd/compute.rs:13:13
    |
13  |     spec fn all(self, p: spec_fn(int) -> bool) -> bool;
    |             ^^^

It seems okay with passing in a closure instead:

 r.all(|v| property_bounds_for_smallest_bitting_size(v)) 

but that makes subsequent triggering more annoying; i.e., I end up writing:

    assert({let r = 0..11int;
            r.all(|v| property_bounds_for_smallest_bitting_size(v))            
            }) by (compute);
    let prop = |v| property_bounds_for_smallest_bitting_size(v);
    assert(prop(size));

instead of what I'd like to write, which is:

    assert({let r = 0..11int;
            r.all(property_bounds_for_smallest_bitting_size)
            }) by (compute);
    assert(property_bounds_for_smallest_bitting_size(size));

[tjhance]

The problem is that we need to coerce the named function to the spec_fn. Unfortunately, it's impossible to tell syntactically if something needs this coercion.

It might be possible to define spec_fn(A) -> B to be dyn Fn(A) -> B or something. But this might interfere with future plans for real dyn, so I'm wary of committing to something like that.

[parno]

Unfortunately, it's impossible to tell syntactically if something needs this coercion.

Could we add syntactic support for the developer to explicitly coerce it? E.g.,

property_bounds_for_smallest_bitting_size as spec_fn(int) -> bool

[tjhance]

You can do closure_to_fn_spec(property_bounds_for_smallest_bitting_size), though it'll look kind of silly since it's not a closure.

[tjhance]

Wait, that might not work. I think closure_to_fn_spec is a magic builtin that really only works for closures. It could be made to work, though.

[parno]

Wait, that might not work. I think closure_to_fn_spec is a magic builtin that really only works for closures.

Indeed. It rather reasonably objects:

error: the argument to `closure_to_spec_fn` must be a closure