[Lean] Passing arrays as slices

[abentkamp]

We produce ill-typed Lean terms when passing arrays into (mut) slice arguments:

fn f(out: &mut [u8]) {
}

fn g(out: &mut [u8; 200]) {
    f(out);
}

Open this code snippet in the playground

@[spec]
def f (out : (RustSlice u8)) : RustM (RustSlice u8) := do (pure out)

@[spec]
def g (out : (RustArray u8 200)) : RustM (RustArray u8 200) := do
  let out : (RustArray u8 200) ← (f out);
  (pure out)

[maximebuyse]

This is because the F* backend encodes arrays and slices in the same type, allowing the to be interchangeable. It was also the case for Vecs, but I changed that when switching to core models, adding this phase. We could adapt the phase to make array <-> slice conversions also explicit.

[abentkamp]

I haven't been able to figure this out. Array seems to trigger the insertion of unsize instead of deref, but inserting this code in the phase you pointed me to didn't work:

| {
             e = App { f = { e = GlobalVar f; _ }; args = [ inner ]; _ };
             typ = TSlice _ as t;
             span;
            }
              when Ast.Global_ident.eq_name Rust_primitives__unsize f ->
                UA.call Core__array__Impl_23__as_slice [ inner ] span t

Instead, I will use the following workaround for now:

fn f(out: &mut [u8]) {}
fn g(out: &mut [u8; 200]) {
    f(&mut out[..]);
}

[maximebuyse]

The frontend and importer produce: f(rust_primitives::unsize(&mut (deref(out)))). deref is removed by phase AndMutDefSite and the unsize by DirectAndMut, so anything we do relying on them should happen before these phases (ExplicitConversions comes after).

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.