-
Notifications
You must be signed in to change notification settings - Fork 9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
requirements for const-eval
#2
Conversation
|
||
## Requirements | ||
|
||
For this to work, const operations have to be both pure and deterministic, at least when they are used in the type system. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"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. :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 ❤️
|
||
Other sources of non-determinism are allocations. This non-determinism | ||
must however not be observed during const-evaluation (TODO: link to const-eval) | ||
and is only an issue if allocations leaked into the result. This |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Using floats during CTFE is fully determinstic. So using | ||
them inside of the type system is fine. CTFE can however | ||
produce different results than what would happen on real hardware, | ||
but this is not a concern for const generics. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
|
||
Other sources of non-determinism are allocations. This non-determinism | ||
must however not be observed during const-evaluation (TODO: link to const-eval). | ||
Any references used in a constant are considered equal if their targets are equal, which is also determistic. (ref [val-trees](https://github.com/rust-lang/rust/issues/72396)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yeah, the giant mess which is structural match ✨
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 ^^
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 ensureT
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
44238bb
to
a7e5aa4
Compare
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 '^^ |
only the second commit is relevant, this is based on top of #1.
@oli-obk @RalfJung can you help me out with the
FIXME
s 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.