requirements for const-eval

[lcnr]

only the second commit is relevant, this is based on top of #1.

@oli-obk @RalfJung can you help me out with the FIXMEs here?
While I think that we don't have to worry about any of these I also
don't know enough to explain why this is the case.

[RalfJung]

"pure" is an observational notion, so the question here is -- pure for which kind of observer? (To give an example: Haskell is very impure if you go down to the level of lazily evaluated thunks and forcing.)

I think the best way to organize this is to have a "value tree" representation of CTFE results, and only that representation will be observed by the type system. Value trees contain no AllocId, which are the only source of impurity in CTFE. (And non-determinism does not arise in CTFE at all.) So I think on this level, CTFE is pure, even with allocations and all that, and by only using value trees, we ensure the type system does not accidentally use AllocId in any way.

Converting a CTFE result to a value tree can fail (this is a "dynamic check" that the CTFE result is indeed consumable in a pure way); you might want to have extra static checks to ensure that this dynamic check never fires -- basically, the return type must not contain raw pointers, fn pointers, floats, or anything else that we cannot convert to a value tree (trait objects?).

See this issue and this hackmd for some more notes on value trees. Those are very terse, so if clarification is needed, please ask. :)

[lcnr]

yeah, "pure" in that the output of CTFE does not depend on any global state, reworded this. ^^

I am still not sure on how in depth I want to go here, so I think I am going to leave the document like this for now.

Thanks for the elaborate answers ❤️

[RalfJung]

Valtrees are not about "not leaking allocations to the result". The point of a valtree is that a value of type &i32 is identified only by the value it points to, not the location in memory. So two &i32 are considered equal if they point to equal things, even if these equal things are located at different addresses.

This is what PartialEq does anyway, but in the compiler, the result of a CTFE query is typically represented as an Allocation and comparing those will also compare the underlying (abstract) addresses.

[lcnr]

Ah yeah, messed this up 👍 Was thinking about how we deal with mutable references which isn't too related to val trees.

Thinking about this, how do we intend to deal with the following:

#![feature(const_generics)]
fn foo<const N: &'static i32>() -> usize {
    N as *const i32 as usize
}

fn bar<const M: &'static i32>() {
    assert_eq!(M as *const i32 as usize, foo::<M>());
}

fn main() {
    foo::<{ &3 }>();
    bar::<{ &3 }>(); 
}

playground
Here we have two different anonymous constants which potentially create different allocations for 3.
These do result in the same valtrees though and should be considered equal by the type system.

This means that during monomorphization we should end up with only one instance for foo. I want to guarantee that this program does not panic, but how do we assert that we only have one unique allocation for all references to 3 used in types? Especially if we codegen foo in different crates.

[RalfJung]

how do we assert that we only have one unique allocation for all references to 3 used in types

We don't, and we don't need to.

The point of valtrees is that we convert the CTFE result to a valtree, and use valtree equality tests only in the type system. So it won't matter if the two allocations with 3 in them have the same address or not; the result valtree will be the same either way.

[RalfJung]

I want to guarantee that this program does not panic

Oh, I missed that part. No that won't be possible I'm afraid. If programmers "look behind the curtain" of the notion of equality we use, they have to deal with the consequences... we currently make no guarantees whatsoever for address identity in const, and I don't see what guarantees we could provide.

It is already the case that if you have regular const of reference type, and cast those to ptrs and compare them, we don't guarantee the result.

[RalfJung]

The caveat here is: there are some proposals to make CTFE raise an error when a float operation produces a NaN (this would avoid producing a result different from real hardware). So this could be relevant in the context of ensuring that there are no post-monomorphization errors.

[RalfJung]

Yes that works. :) It might be worth pointing out that raw pointers and function pointers must not be allowed, since they cannot be compared this way. Same for &dyn Trait I think.

[lcnr]

yeah, the giant mess which is structural match ✨

[lcnr]

luckily it's not too bad for const generics cause we don't have to care about structural match for values as we only look at types.

iirc dealing with consts in patterns is the actual hard part ^^

[RalfJung]

yeah, the giant mess which is structural match sparkles

I wasn't even talking about that.^^ But I hope valtrees can help fix that, too.

luckily it's not too bad for const generics cause we don't have to care about structural match for values as we only look at types.

I don't follow. You care about when two values of some type T are equal. You care to do that deterministically. So you should ensure T does not involve raw pointers, function pointers, or trait objects.

[lcnr]

the way we forbid &dyn Trait and raw pointers is by checking that the types implement structural match.

I don't follow. You care about when two values of some type T are equal. You care to do that deterministically. So you should ensure T does not involve raw pointers, function pointers, or trait objects.

As far as I know None::<NonStructuralMatchTy> is an allowed as a pattern. So for patterns we also use control flow analysis to check if a value can be used. At least that's what I infer from rust-lang/rust#67343 and rust-lang/rust#73448, didn't interact with that for a while.

This does not matter for const generics, as even if enum variants which are structurally match exist for a type, that type can still not be used as a const parameter type.

[RalfJung]

Oh, that's what you mean. Sure, the valtree framework can handle None::<T> for any T -- what really matters is if you can construct a valtree for the given value, i.e., it matters whether the given value contains a raw pointer, function pointer, or trait object. The type-based analysis just overapproximates that property.

[lcnr]

as it is, this pr is already a bit useful and can be extended later, so i am just going to merge this, don't think keeping this open for another year makes much sense '^^