Array/slice encoding

[Aurel300]

(requires prusti/pcg#120)

[Aurel300]

These transmutes are obviously not great... I guess one "proper" solution would be for the implementors of the shared trait to define their own lift function which would either be a no-op (when Curr = (), Next = !), or a lift call (when it's the pure function encoder's ExprRet). I wonder if this comes up often enough? Thoughts @zgrannan?

[zgrannan]

Hmm, so it looks like the 2nd transmute is doing the opposite of a lift? Its taking an ExprGen<Curr, Next> and turning into an ExprGen<(), !>.

I think maybe the other direction makes more sense (and may solve a more general version of this problem)

We can use .call() to get this:

let unsize: FunctionIdnGen<'vir, Self::ExprCurr, Self::ExprNext, (vir::CSnap, vir::ManyTyVal, vir::ManyCSnap), vir::CSnap> = self
    .deps()
    .require_ref::<MirBuiltinEnc>(MirBuiltinEncTask::Unsize(from_ty, ty, def_id))?
    .unsize()
    .unwrap()
    .call();

then the problem becomes:

let expr: vir::ExprGenSnap<'vir, Self::ExprCurr, Self::ExprNext> = unsize(
  encoded_operand.downcast_ty(),
  generics.ty_exprs(),
  generics.const_exprs(),
)

where the latter two have type &[vir::ExprTyVal<'vir>] instead of
&[vir::ExprGen<'vir, Self::ExprCurr, Self::ExprNext, TyVal> (and CSnap resp).

So we can define a general lift operation like:

pub(crate) trait LiftsTo<T> {
    fn lift(self) -> T;
}

impl<'a, 'vir, Curr, Next, T: CompType> LiftsTo<&'a [vir::ExprGen<'vir, Curr, Next, T>]>
    for &'a [vir::Expr<'vir, T>]
{
    fn lift(self) -> &'a [vir::ExprGen<'vir, Curr, Next, T>] {
        // SAFETY: See ExprGenData::lift
        unsafe { std::mem::transmute(self) }
    }
}

Not sure if this transmute is safe tho

[JonasAlaif]

note that I don't think that we run the v2 tests in the ci anymore

[Aurel300]

We don't, but I wanted a self-contained test file for the array/slice features I was implementing. We can eventually add this to the v1 test suite. Note that this test currently passed but a precondition is commented out: it can be made to pass by adding an assertion in the Viper encoding that causes a quantifier to be triggered, so I think the trigger in the "undo unsize" method might be too restrictive.