Clarify the encoding of closures

[Nadrieril]

As of https://github.com/AeneasVerif/charon/pull/186, closures are implemented by letting the consumer of llbc track which function pointer goes with which closure, and the Call terminator mentions a built-in trait implementation for Fn/FnMut/FnOnce that the consumer of llbc must deduce corresponds to the aforementioned function pointer.

I propose that we instead encode this:

pub fn test_closure_capture(x: u32, y: u32) -> u32 {
    let f = &|z| x + y + z;
    (f)(0)
}

as follows:

struct {test_closure_capture::closure#0} {
    x: u32,
    y: u32,
}

impl Fn<(u32,)> for {test_closure_capture::closure#0} {
    type Output = u32;
    fn call(&self, arg: (u32,)) -> u32 {
        self.x + self.y + arg.0
    }
}

pub fn test_closure_capture(x: u32, y: u32) -> u32 {
    let state = {test_closure_capture::closure#0} { x, y };
    state.call(0)
}

This is pretty much exactly how rustc represents closures internally, and has the benefit that consumers of llbc don't need to do anything special to support closures.

[sonmarcho]

Small update: after a discussion I think we came up with a different solution, where the function pointer is not stored in the state but in the instance of Fn<(u32,)> (maybe it is actually what you mean above, but it is slightly unclear).

[Nadrieril]

That is indeed what I meant above; as you can see, there is no function pointer stored anywhere in the desugared output; the special closure type is just the name for a struct.

[ssyram]

Hi, I'm also curious about how is this issue now. I think the current LLBC has not yet extracted the new closure struct. Also, I found that currently LLBC has a special case (Aggregate (AggregatedCLosure (...))) specifically for this case. I think it would be desirable to handle closures as an impl call for usual struct -- as already translated in MIR?

[Nadrieril]

This is indeed what we plan to do. Subscribe to this issue to be kept up to date :D If this is particularly important for your usecase, come chat on the aeneasverif Zulip.

[ssyram]

Thank you! I think the best way to handle this is that, we view every Fn series (FnMut/Fn/FnOnce) as pure traits & function calls. Hence there should be no extra effects to put on these cases but simply treating them with usual traits machanisms. But fn should be treated differently -- the arrow types should be used solely on fn. Is this the idea? By the way, this is not particularly urgent in my usecase, but I just want some completeness guarantee...

[Nadrieril]

I don't know what you mean by "effects", but absolutely we plan to treat them with the usual trait mechanisms.

Arrow types should be used only for fn yep, the fact that they're used for closures today is leftover from the initial implementation that was focused on outputting functional languages (that don't distinguish closure types from function types) and I really want to get rid of it.

[ssyram]

Sorry, "effects" => "efforts"...

Thanks for the clarification, this is pretty clear now! And yes, I think it is absolutely great to handle the stuff with this clean separation.