Error when using pure functions that return a reference

[juliand665]

When you use a pure function that returns a reference to an associated type (like e.g. Deref::deref does), you get an error like "There is no procedure contract for loan bw3. This could happen if you are chaining pure functions, which is not fully supported.", even though there doesn't appear to be any chaining going on. I've reduced it to a minimal example with no external types or extern specs:

trait Foo { // similar to Deref
    type Bar;
    
    // not necessary for error:
    //#[pure]
    fn bar(&self) -> &Self::Bar;
}

impl Foo for i32 {
    type Bar = i32;
    
    #[pure]
    fn bar(&self) -> &Self::Bar {
        &self
    }
}

fn main() {
    let v = 1;
    let _ = v.bar();
}

This is the specific error it produces:

It doesn't seem to matter whether you use the function as a member or a free function (like Foo::bar(&v)). Also—though this might just be a product of how the encoding is performed—the error does not appear at the call site if the value is used later on, e.g. like this:

[juliand665]

@Aurel300 since you wanted to look into this :)

[Patrick-6]

This example causes a very similar error, but it uses a reference to an i64 and not to an associated type:

use prusti_contracts::*;

#[pure]
fn fn_a(x: &i64) -> &i64 {
    x
}

#[pure]
fn fn_b(x: &i64, i: u64) {
    if i != 0 {
        fn_b(&fn_a(x), i - 1);
    }
}

[Prusti internal error] Prusti encountered an unexpected internal error
Details: There is no procedure contract for loan bw6. This could happen if you are chaining pure functions, which is not fully supported.

[juliand665]

Update—I found an even simpler MWE than my posted one, no traits or associated types needed:

fn main() {
    let foo = Foo { x: 42 };
    let x_ref = *foo.x_ref();
}

struct Foo {
    x: i32,
}

impl Foo {
    #[pure]
    fn x_ref(&self) -> &i32 {
        &self.x
    }
}

So I think @Patrick-6's example is indeed this issue as well.