🚲🏠 Renaming validity and safety?

[Centril]

It has been noted on several occasions, e.g. rust-lang/rust#53491 (comment) and rust-lang/rust#53491 (comment) that "valid" is prone to confusion with "safe" due to the way the former sounds. In particular, it raises the question "Valid with respect to what"?

Thus it is probably a good idea to rename one or the other into something else.

@RalfJung suggested "initialization invariant" (because any initialized T must satisfy such invariants) as a replacement of "validity invariant" while I suggested "machine invariant" (because it signifies the invariants the abstract machine requires of a T). If we rename validity to either of those then "safety" might not need renaming; but if it does, "type system invariant" may be one candidate.

[RalfJung]

One reason why I suggested "initialziation invariant" is because it connects with MaybeUninit.

MaybeNoMachine doesn't really roll very well...

[RalfJung]

Also note that the validity invariant only applies to data that the compiler considers initialized -- this has been a point of confusion several times. Having something with "initialization" in its name should help clarify that.

[RalfJung]

In the MaybeUninit docs I am talking about the "initialization invariant". But I have since regretted that choice, because e.g. a MaybeUninit<u32> is actually "initialized" in uninitialized memory -- and we might end up actually allowing the same for u32.

"Machine invariant" seems like a reasonable choice. But then MaybeUninit should be MaybeMachine?^^

[Ixrec]

On one or two past threads I've suggested that we use "sound" to mean "has defined behavior" and "unsound" to mean "is UB", and I still think that's a good idea. So by analogy, I'd suggest renaming the "validity invariant" to the "soundness invariant". At least to me, that makes it immediately obvious what it's supposed to mean: if you violate this, then your code is broken, full stop.

Regardless of which particular word we choose, I do think that it's strongly desirable that "X-ness invariant" corresponds to "if your code is X, it does not have UB". I would not be surprised if "sound" and "unsound" have different connotations to other people and we have to come up with something else, but if we end up agreeing on (for example) "validity invariant" for this, I believe we should also agree to start using "valid" with the very specific meaning of "does not have UB".

IMO, that's the biggest disadvantage of "initialization" or "machine" invariant: it clearly doesn't make any sense to say "if your code is initialized/machined, it has no UB", so we can't hope to kill two birds with one piece of jargon that way.

Also, to me "machine invariant" sounds very strongly like it's trying to distinguish hardware properties from software properties, which is presumably not a distinction the Rust abstract machine would make. It didn't even occur to me the "machine" in "machine invariant" might refer to the Rust abstract machine until I re-read Centril's comment above.

[gnzlbg]

On one or two past threads I've suggested that we use "sound" to mean "has defined behavior" and "unsound" to mean "is UB", and I still think that's a good idea. So by analogy, I'd suggest renaming the "validity invariant" to the "soundness invariant". At least to me, that makes it immediately obvious what it's supposed to mean: if you violate this, then your code is broken, full stop.

Code that does not violate this isn't necessarily sound, e.g., if it violates the safety invariant.

[gnzlbg]

@RalfJung suggested "initialization invariant" (because any initialized T must satisfy such invariants) as a replacement of "validity invariant" while I suggested "machine invariant" (because it signifies the invariants the abstract machine requires of a T).

"Initialization" is super confusing. The other day some reddit users where super confused about why this is always correct: MaybeUninit::<MaybeUninit<T>>::uninit().assume_init().

Their argument was that the documentation of MaybeUninit<T>::assume_init() says that if the T is not initialized, the behavior is undefined. Some people were trying to explain them that "uninitialized memory is initialized" but that obviously did not go very far. I can't blame them.

This issue was raised multiple times during the RFC, FCP, etc. of MaybeUninit and I still have no idea why we ended up in a place where we have to explain people in Rust that sometimes "uninitialized memory is initialized", but I rather don't introduce the same issue in the UCGs. If someone wants to introduce the same issue here, they should IMO make a case again for it.

I'm personally fine with using the term "validity", and I believe that any Rust programmer dealing with unsafe code and uninitialized memory is smart enough to learn a new word and its meaning, particular a word that is used many times throughout the spec.

This means that when reading the spec they will probably have to first unlearn the "initialization" terminology used in the API docs, then learn a new word and its meaning, and afterwards mentally replace "initialization" in the API docs everywhere with that word for anything to make sense ("uninitialized memory is initialized" vs "uninitialized memory is valid at type T").

This situation is unfortunate, but better than introducing here another overloaded term like "machine" that might end up confusing users in different ways that "initialization" does today.

---

"Machine invariant" seems like a reasonable choice. But then MaybeUninit should be MaybeMachine?^^

What does the Maybe_ prefix tries to achieve ?

Why can't it just be Uninit<T> or Invalid<T> with an ::assume_valid method ?

A Machine<T>/MaybeMachine<T> with an ::assume_machine method is IMO much weirder than Invalid<T>. I wonder how this will impact the readability of the text. We currently use "valid"/"invalid" in a lot of places in the text and discussions, and with machine we would need to use "machine"/"not machine" or similar.

[RalfJung]

On one or two past threads I've suggested that we use "sound" to mean "has defined behavior" and "unsound" to mean "is UB", and I still think that's a good idea.

I disagree strongly. Why invent new terms for something that already has a term, namely, "has (no) UB"? If "has no UB" sounds too negative, an alternative positive wording I sometimes use is "has well-defined behavior".

Worse, "sound" is already used to mean something else: A safe function / API is unsound if it is possible for safe code using it to cause UB. Otherwise, it is sound.
So, soundness is a property of a library; having UB is a property of a program. @gnzlbg already used "sound" the same way up there. I'd appreciate if we could be consistent about this -- let us not burn terms by using them in different ways for no good reason.

EDIT: I propose we add this term to the glossary: #190

it clearly doesn't make any sense to say "if your code is initialized/machined, it has no UB", so we can't hope to kill two birds with one piece of jargon that way.

"code" isn't "initialized", that makes no sense indeed. But I think this is actually in fact another argument against your terminology: code can have UB in other ways than violating the validity invariant! Say we have code that uses unchecked_add to cause an overflow, but the validity invariant is always satisfied. This code has UB. It would be very confusing if the invariant and UB-ness used related terms.

[RalfJung]

"Initialization" is super confusing. The other day some reddit users where super confused about why this is always correct: MaybeUninit::<MaybeUninit>::uninit().assume_init().

I admitted exactly that a few posts up. :)

This issue was raised multiple times during the RFC, FCP, etc. of MaybeUninit and I still have no idea why we ended up in a place where we have to explain people in Rust that sometimes "uninitialized memory is initialized"

The name of what is now called assume_init was heavily bikeshed. Nobody suggested a better name. Pretending like you don't understand the process at which we arrived here is disrespectful of everyone involved.

Multiple people reviewed the stablization PR and also the others about documenting MaybeUninit, renaming assume_init, all of that. The reason this wording stuck is that nobody proposed a better one.

Yes, you raised a concern related to this. You made an "excruciatingly verbose" proposal but said yourself "I don't know whether the painfully excruciating approach is worth pursuing". And moreover, it's not even the same concern -- that one was about validity not being enough because there is also the safety invariant, now the issue is that "uninitialized memory" can be considered initialized. I do not think anyone raised that particular concern before stabilization. Prove me wrong.

I'm personally fine with using the term "validity"

The issue is that "this is a valid Vec<T>" will likely often be read as "oh so it's safe to use it". This was discussed pre-stabilization. People seemed to prefer MaybeUninit over MaybeValid. I would have been fine to go either way, but it's a bit late for that now.

Why can't it just be Uninit or Invalid with an ::assume_valid method ?

This was discussed pre-stabilization, the argument was that Uninit<T>/Invalid<T> sounds like this is definitely uninitialized/invalid, which is not true.

I wonder how this will impact the readability of the text. We currently use "valid"/"invalid" in a lot of places in the text and discussions, and with machine we would need to use "machine"/"not machine" or similar.

"machine" is indeed not suited as an adjective. We'd have to find another short-hand for "satisfies the machine invariant".

This means that when reading the spec they will probably have to first unlearn the "initialization" terminology used in the API docs, then learn a new word and its meaning, and afterwards mentally replace "initialization" in the API docs everywhere with that word for anything to make sense ("uninitialized memory is initialized" vs "uninitialized memory is valid at type T").

We will have to disentangle "(un)initialized memory" from "(un)initialized variable (of type T)". Not great, but I think it can be done. "A variable of type T is initialized if it satisfies the validity invariant", or so.

[gnzlbg]

Yes, you raised a concern related to this. You made an "excruciatingly verbose" proposal but said yourself "I don't know whether the painfully excruciating approach is worth pursuing". And moreover, it's not even the same concern -- that one was about validity not being enough because there is also the safety invariant, now the issue is that "uninitialized memory" can be considered initialized. I do not think anyone raised that particular concern before stabilization. Prove me wrong.

People in that thread were confused about the "initialized" vs "validity invariant" semantics of "into_init" because it has "initialized" in its name. I thought this issue was important enough to raise it in the first sentence of the comment you just cited: "I think it is worth it to call out again that the only thing that into_init asserts is that the value satisfies the validity invariant of T, which is not to be confused with T being "initialized" in any general sense of the word."

I proposed using Invalid<T> with into_valid instead, but this was briefly dismissed here: rust-lang/rust#53491 (comment): "This is correct. OTOH, I feel "initialized" is a reasonable proxy for this in a first explanation."

I felt the issue fell in deaf ears, and the throughput of the discussion was too high for me to keep up with it, so I left it at that.

So this precise issue was raised there and known, and from what I understood it was an explicit design decision to use "initialized" instead. Even though it could be confusing, as that discussion showed.

[RalfJung]

"I think it is worth it to call out again that the only thing that into_init asserts is that the value satisfies the validity invariant of T, which is not to be confused with T being "initialized" in any general sense of the word."

You are quoting without context. The post goes on demonstrating the issue with an example of something that satisfies the validity invariant, but not the safety invariant. So, my reading of what you said -- and I still interpret your post the same way when I re-read it now -- is that "initialized" above means "safety invariant". Your concern (or rather, my interpretation of your concern) was that someone could "initialize" a Vec<T> (or an AlwaysTrue in your example) but fail to actually make it a safe instance of that type. To account for this, an appropriate paragraph was added to the MaybeUninit docs.

If you meant that particular post to raise the concern that "uninitialized memory can be initialized because some validity invariants allow that", then we heavily miscommunicated. As far as I can see, nothing in your post indicates that you are worried about the interaction of uninitialized memory and assume_init.

I proposed using Invalid with into_valid instead, but this was briefly dismissed here: rust-lang/rust#53491 (comment): "This is correct. OTOH, I feel "initialized" is a reasonable proxy for this in a first explanation."

I was responding to the issue that Vec<T> can be "initialized" without being safe to use -- we can satisfy the validity invariant, which makes assume_init non-UB, but fail to satisfy the safety invariant, so e.g. dropping that vector will cause UB. I still think "initialized" is a reasonable proxy here.

Note that this is not the problem that is biting us now. MaybeUninit::<MaybeUninit<T>>::uninit().assume_init() is fine both from a validity and safety invariant perspective, so there is not even an overlap with the issue you raised in that post. The problem we are having now is specifically about uninitialized memory being valid for some types (0xUU, in my terminology). Uninitialized memory during assume_init AFAIK never came up in the pre-stabilization discussion.

into_valid was part of your "excruciatingly verbose" proposal (your terms), and then of another proposal involving two types and two traits, which I would also call "excruciatingly verbose". I have not seen a proposal to keep the API as it was but just rename assume_init to assume_valid or so. AFAIK, nothing involving valid was suggested during the into_inner bikeshed. It is sure possible I missed that though.

[RalfJung]

The other problem with enshrining "valid" anywhere in the API is that there is no consensus yet (that I know of) that this is the term we want to stick to -- source: this issue is still open.

I'd be totally up for that. Of course the API is fixed now (we could consider renaming assume_init, but we should wait at least a year or two otherwise this looks silly), but the docs could use this term.

If we decide that the validity invariant arises from typed copies alone, another good term might be "representation invariant": in that case, a bit string is "valid" for a type if and only if the bit string represents some value at the type. However, this would preclude some options in #77: the representation relation is "pure" and cannot demand things like "the pointer must not be dangling" or "the pointer must point to memory that is valid for T".

[gnzlbg]

So, my reading of what you said -- and I still interpret your post the same way when I re-read it now -- is that "initialized" above means "safety invariant".

If this is the case, you are completely misunderstanding both the post, and also the confusion that the users in that thread had back then, as well as the confusion that people still have now.

By "initialized"/"uninitialized" most users just mean whether that memory was touched or not (was something written to it?). They don't know that there are things like "validity" or "safety" "invariants", or any other kind of "invariant" for that matter.

They are literally just confused that the memory was not touched or written to, therefore it is uninitialized, and claiming that it is initialized is incorrect, becasue that would mean that something was written to it, even if it is all just zeros (independently of whether anything has to be written at all).

[gnzlbg]

To expand, the confusion of users is orthogonal to whether something must actually be written at all, or whether what's written satisfies the validity or safety invariants, e.g., many users do believe that

let mut x: MaybeUninit<T> = MaybeUninit::uninit(); // x is uninitialized
x = MaybeUninit::zeroed(); // x is initialized

holds for all T because they see it only from the POV of whether something was written to the memory. They don't look at this from the POV of a safety or validity invariant, mostly because they do not know that such a thing exists.

[RalfJung]

If this is the case, you are completely misunderstanding both the post, and also the confusion that the users in that thread had back then, as well as the confusion that people still have now.

I don't recall anyone being confused about this (uninitialized memory), do you have pointers?

And I do understand that the discussion right now is about uninitialized memory. But where does your post, your example back then indicate that you are worried about uninitialized memory? The example specifically was about creating an instance of a type that is valid but not safe. We do agree that that is not the issue right now, right?

We have two confusions about assume_init:

• The Vec<T> case:

  let mut u = MaybeUninit::<Vec<T>>::uninit();
  u.as_mut_ptr().write_bytes(1u8, 1);
  let v = u.assume_init(); // no UB here: this is valid!
  drop(v); // but it's not safe, so there is UB here.

  You raised this before, you gave the AlwaysTrue example, but I considered this to be fixable by docs. People were confused about this, yes. But the proposed alternatives were very complicated APIs that even you admitted were probably overcomplicating things.
• The "nested MaybeUninit" case:

  let mut u = MaybeUninit::<MaybeUninit<T>>::uninit();
  let v = u.assume_init(); // no UB here: this is valid!
  // And in fact this is also safe, we could run any safe code here

  This only came up after stabilization. The fix could have been to call this assume_valid or so, but that wasn't proposed (or rather, only proposed as part of the much more complex proposals trying to solve the Vec<T> case).

I think these are very distinct cases. In the first case memory is initialized, it is even valid, but then the issue is that there's another invariant, the safety invariant, that is violated. In the second case, memory is not initialized and yet it is valid.
The fact that these are distinct is also evident in the observation that fixing them requires very different measures to be taken. The first requires teaching the two invariants, the second does not.

If you meant to raise the "nested MaybeUninit" problem in that post, you seriously failed to express that.