Clarify UB around immutability & mutation

[ivanbakel]

I personally found this description of UB confusing, since the use of "reached" suggests that UB only happens for read bytes, and the definition of immutability is not given, allowing for multiple interpretations: does the "data" have to be immutable from the first read? From the creation of the reference? Between reads from the immutable accessor, but not otherwise? etc.

This clarifies the actual UB conditions, based on this Zulip interaction and this reference discussion in two ways:

• The definition of "data" is clarified to be stated in terms of bytes, in a way that should avoid ambiguity about which bytes are considered. Based on the GH issue, this clarification should also allow for use of a *mut pointer through a shared reference, which is not in itself UB. Based on the Zulip issue, the definition includes padding bytes, which may be surprising.
• The definition of immutability & mutation for a set of bytes is clarified to mean forbidding all non-0-byte writes.

---

I also tried to avoid use of the word "reachable", since I thought it be implying a transitive property about immutability for references which (to my understanding) doesn't actually apply. This may now fail to cover mutable-references-behind-shared-references in some way, but I'll leave it to review to decide that.

[ehuss]

cc @RalfJung Do you have a chance to review this?

[RalfJung]

Hm... not sure. This includes things which I would say are commentary, and already implied by the previous sentence which is the actual spec (such as the remark about padding, or the last sentence about writes not modifying the byte's contents). We should at least clearly separate comments from spec -- we don't want to leave the impression that the sentence "Writes which do not modify the byte contents are still mutations" changes the definition of "mutation".

Also, "bytes of a value pointed to by a shared ref" is IMO even less clear than the previous formulation. What about just saying "bytes pointed to by a shared ref"? Then IMO the sentence about padding becomes unnecessary. If anything we might want to define "pointed to" -- which we actually kind of do define later

The span of bytes it points to is determined by the pointer value and the size of the pointee type (using size_of_val).

---

Based on the Zulip issue, the definition includes padding bytes, which may be surprising.

When talking about bytes, there isn't even such a thing as "padding bytes". They only exist when talking about values and how those relate to their byte representation.

By rephrasing the entire definition in terms of bytes, I don't think we still need the padding comment -- it is redundant.

[RalfJung]

This may now fail to cover mutable-references-behind-shared-references in some way, but I'll leave it to review to decide that.

Yeah that's a good question. Maybe add something like "all bytes pointed to by a shared reference, including transitively through other references (shared and mutable) and Boxes, including those stored in fields of compound types"?

This isn't even the bullet point about the aliasing model, but I think the old "reached" was intended to capture this transitivity. (The term goes back all the way to the initial commit, so it's hard to tell.)

[ivanbakel]

This includes things which I would say are commentary, and already implied by the previous sentence which is the actual spec (such as the remark about padding, or the last sentence about writes not modifying the byte's contents). We should at least clearly separate comments from spec -- we don't want to leave the impression that the sentence "Writes which do not modify the byte contents are still mutations" changes the definition of "mutation".

I originally had these as notes, but I was worried about over-bulking the section. I can move the unchanged-value addendum back to a note, but I'm certain it's surprising enough to include explicitly. The padding note can be removed when moving to the byte-based definition; but it's worth dropping any mention of "data" then, since I think it's confusing (if bytes are what really matter.)

Yeah that's a good question. Maybe add something like "all bytes pointed to by a shared reference, including transitively through other references (shared and mutable) and Boxes, including those stored in fields of compound types"?

I will add that.

[RalfJung]

LGTM.

[ehuss]

Thank you @ivanbakel and @RalfJung!