Add more precise Slice bounds

[cole-k]

All slices have 0 <= len <= usize::MAX, with the upper bound subject to overflow checking.

Also subject to overflow checking, slices have len * T::size_of() <= isize::MAX (see std::slice::from_raw_parts).

While this holds for all slices, the above condition reduces to true for ZST slices, so we omit it. Additionally, for ZST slices, the usize::MAX upper bound is redundant, so we omit it.

The implementation achieves this in a manner akin to how you'd do it if you wrote it on an extern spec (i.e. referring to T::size_of() directly), although it can branch on whether T is ZST better.

[cole-k]

This is the only spot that seems to require the genv. Could it be skipped somehow?

[cole-k]

This happening unconditionally caused an ICE that is hopefully now fixed in vtock.

The issue is that we would have a param for T::size_of() in the invariants for slices and if the T was legitimately generic it would wrongly be substituted (and crash) in this code.

Changed it so that only BaseTy::Adt actually does the substitute.

[nilehmann]

Why compute the layout here? can you express it in terms of T::size_of()?

[cole-k]

I could, but then for ZSTs we'd have an unnecessary T::size_of() * len <= isize::MAX and for non-ZSTs we'd have a redundant len <= usize::MAX.

I almost opted to avoid the T::size_of() and just use the size directly in the constraint, but I figured just in case we change how the assoc reft behaves it would be safer to use it...

Seeing the weirdness with actually defining T::size_of() in Flux below, maybe it would be better to just "inline" the size directly in the constraint?

[nilehmann]

I'd only keep the T::size_of() * len <= isize::MAX to make T::size_of() the only place where we compute sizes. For zero-sized types, it'll normalize to 0 * len <= 9223372036854775807, so I don't think Z3 will have problems with it, and we could eventually constant-fold it

[cole-k]

What about the redundant len <= usize::MAX? I guess I no longer really see the concern with T::size_of() diverging from the "inlined" slice specs.

What if I factored out a function from builtin_assoc_refts.rs that evaluates T::size_of() and called it when building the slice invariants to build the specialized ones?

If you'd prefer it to be just T::size_of() * len <= isize::MAX && len <= usize::MAX always, then I'll go that route. But this also skips having to hack stripping the refts from T ;)

[nilehmann]

I prefer that T::size_of is the only place where we compute sizes. Also, I don't think len <= usize::MAX is redundant if T is generic, because if you don't know what T is, then you cannot derive len <= usize::MAX.

[cole-k]

Ah true, might even be ZST. OK fine, I'll switch the specs to the above then and try your hack for dropping the refinements.

[nilehmann]

damn, this is problematic. I think we would run into trouble with something like

#[flux_rs::spec(fn(x: &[{v. (i32, i32[v])}]))]
fn foo(x: &[(i32, i32)]) {}

Instead of skipping existentials, we should erase refinements.

[cole-k]

Can you cook up something that fails?

Your test seems like it passes. I checked and it does seem like it's incorrectly keeping the index around, but also that said index isn't causing problems.

I'll need a hint to figure out how to erase the refinements, since I already had to use some computerized assistance to get the types to line up here. Although now that I look at it, we could also just use GenericArg::Ty which also works on my tests, but I'm guessing that is even worse because using it that way doesn't erase anything?

---

Actually, from what I gather, if we're already calling to compute the value of T::size_of() when we resolve the assoc reft

.layout_of(typing_env.as_query_input(elem_ty.to_rustc(genv.tcx())))

then the type itself can have all sorts of refinement junk on it and it'll be fine, right?

Put differently, why would it be bad for T to have refinements on it if we're just gonna send it to its rustc type to get its size?

[nilehmann]

interesting. It doesn't fail, but it creates something nonsensical

#[flux_rs::opts(check_overflow = "strict")]
#[flux_rs::spec(fn(x: &[{v. (i32, {i32[v] | v > 0})}]))]
fn foo(x: &[(i32, i32)]) {}

produces the following as the invariant

<(i32, { i32 | () > 0 })) as Sized>::size_of() <= 9223372036854775807

There's an (implicit) assumption in to_subset_ty_ctor that the type doesn't have escaping variables, so we end up binding the wrong thing.

[nilehmann]

We don't have a good way of erasing refinements here. The best I can think of is

                        .with_holes()
                        .replace_holes(|_, _| Expr::tt())
                        .as_bty_skipping_existentials()
                        .expect("slice element type must have a base type")
                        .to_subset_ty_ctor(),