Dereferencing GhostBox in pearlite: why is inner_logic needed?

[arnaudgolfouse]

The issue

In pearlite, dereferencing a GhostBox can be used to access the inner value:

#[requires(*x == 1)]
fn foo(x: GhostBox<Int>) {}

But sometimes this fails, when using mutable borrows:

#[requires(^*x == 1)]
fn foo(x: GhostBox<&mut Int>) {}

error: unsupported logical reborrow UpvarRef { closure_def_id: DefId(0:10 ~ test[0630]::foo::{closure#0}), var_hir_id: LocalVarId(HirId(DefId(0:9 ~ test[0630]::foo).2)) }, only field projections and slice indexing are supported
 --> ./test.rs:1:14
  |
1 | #[requires(^*x == 1)]
  |

Explanation

That's because the function desugaring is:

fn foo(x: GhostBox<&mut Int>) {
    // #[requires(^*x == 1)] is desugared into:
    let _requires = || {
        fin(&mut *DerefMut::deref_mut(&mut x)) == 1
        //                            ^^^^-- error because of this
    };
}

And this borrow is unsupported in pearlite code. The code we wanted to generate was

fin(GhostBox::into_inner(x)) == 1

Unfortunately the handling of *x in pearlite is a hack, that does not work in this case.

Solution

... ?

Right now the workaround is to use inner_logic:

#[requires(^x.inner_logic() == 1)]
fn foo(x: GhostBox<&mut Int>) {}