Converting between Fn and spec_fn

[Timmmm]

If I have a function that takes a Fn, and I want to involve that in a spec, is there any way to somehow convert it to a spec_fn? Kind of like how you can convert Vec<> to Seq<> with @?

fn retain(v: &mut Vec<u8>, mut f: impl Fn(u8) -> bool)
    requires
        forall|x| 0 <= x < 256 ==> call_requires(f, (x,)),
    ensures
        v@ == old(v)@.filter(f),
{

This gives

17 |         v@ == old(v)@.filter(f),
   |                       ------ ^ expected `FnSpec<(u8,), bool>`, found type parameter `impl Fn(u8) -> bool`

I tried f@ but

22 |         v@ == old(v)@.filter(f@),
   |                               ^ method not found in `impl Fn(u8) -> bool`

[parno]

Unfortunately, it's unlikely we'll have such a feature any time soon. Implementation functions can do lots of things that spec functions can't (e.g., mutate memory, loop indefinitely, or return non-deterministic results). There are some plans under discussion to allow you to go the other way, however.

[Timmmm]

Is there anything I can do in this case then? Or is it impossible to state this sort of property currently?

Like, can I add a constraint that the function is deterministic, pure and total?

I guess I can come up with less exhaustive properties for retain() like that the output must be the input with an arbitrary set of elements removed?

[parno]

Like, can I add a constraint that the function is deterministic, pure and total?

No, I'm afraid that's not supported at present. Instead, you could try to frame your post-condition for retain in terms of the call_ensures for f.