Area proposal: validity invariants #54
Conversation
| * Structs, tuples, arrays and all other aggregates (closures, ...) | ||
| * Is there anything to say besides: All fields must be valid at their | ||
| respective types? | ||
| * The padding between fields can be anything, including uninitialized. It was |
There was a problem hiding this comment.
Are generator fields (and more generally generator contents) exposed to user code at all? If not, this doesn't seem like something UCG have to say anything about, just pure rustc implementation details.
There was a problem hiding this comment.
Are generator fields (and more generally generator contents) exposed to user code at all?
They are not, AFAIK.
But I think when we are in the business of type invariants, we should not forget about types like closures or generators. Just because the user cannot write them directly, doesn't mean their invariants are not important to know -- and compiler devs also need guidance for how to approach validity invariants.
And, of course, unsafe code could start to play games with these fields.
There was a problem hiding this comment.
It's certainly a related issue, but one that interacts with generator implementation details much more than with user-facing guarantees or semantics of Rust-the-language, so I'm not sure the group of people here is the best to discuss it. So I think it would be reasonable to punt on it to reduce the scope of the validity invariant discussion and get it done more quickly. But we could also open the issue for generators and maybe end up wrapping up the discussion without any decisions being made about generators.
And, of course, unsafe code could start to play games with these fields.
Regardless of how generators end up being organized internally, I am quite certain they should be opaque, i.e., user code should not be allowed to poke at their contents in such a way.
There was a problem hiding this comment.
I always reasoned about closures as being equivalent to a struct that one could write by hand (and with feature(fn_traits) one actually can). The rules for building that struct are part of the language, but the layout, validity, etc. of this struct would follow from the layout and validity invariants that we specify here for primitive types, structs, etc.
I would find it extremely weird if the same wouldn't be true for generators. That is, the exact type of the Generator would be unspecified, but this type would be a normal Rust type, e.g., a struct or an union, with normal Rust fields (struct, unions, primitive types, etc.).
Otherwise, Generator would need to be a new kind of thing that isn't a struct, union, etc. and that would probably block people from writing user-defined Generators just like we can build "user-defined" closures.
There was a problem hiding this comment.
we could also open the issue for generators and maybe end up wrapping up the discussion without any decisions being made about generators.
That seems reasonable. And I agree unsafe code shouldn't mess with implementation details of closures or generators, but that doesn't follow from them being in any way different than other struct -- it entirely follows from the fact that unsafe code must not make any assumption about that the struct (its fields etc) looks like.
"user code should not be allowed to poke at their contents in such a way" also applies to many, many other data types -- to pick an example, HashMap (or else we couldn't replace it by hashbrown as is being pursued right now).
|
@RalfJung when you're happy with this, let's merge it |
| This discussion is meant to focus on the question: Which invariants derived from | ||
| types are there that the compiler expects to be *always* maintained, and | ||
| (equivalently) that unsafe code must *always* uphold (or else cause undefined | ||
| behavior)? This is what is called "validity invariant" in |
There was a problem hiding this comment.
I'm curious whether there exist properties that unsafe code must always uphold but which it cannot rely upon. The idea would be: for now, we require that this is true, but we expect we may not require it forever. Technically, from the compiler's POV, we can tweak these predicates because that just makes less code UB -- but unsafe code could be relying on the fact that doing otherwise would be UB, and that could be a problem.
This seems like a more general thing -- it also e.g. arises in the reprsentation discussion -- but once we start getting into invariants, I expect we should think carefully about this distinction.
I would sort of like this to be noted somewhere as a kind of "cross-cutting concern" -- i.e., for each area, we are aiming to define these two predicates (what unsafe code must uphold, and what it can rely on) somewhat separately.
There was a problem hiding this comment.
I agree in general. We want some "wiggle room" in our definition of what unsafe code can do, certainly when it comes to the safety invariant. I am less sure for the validity invariant.
My main problem with this is that I don't have a good understanding yet of how this works formally. That's mostly because I did not spend enough time to think about this.
done |
Which invariants derived from types are there that the compiler expects to be always maintained, and (equivalently) that unsafe code must always uphold (or else cause undefined behavior)? This is what is called "validity invariant" in my blog post.
Goals