Adopt Minimum Union Validity Rules

[chorman0773]

I'd like a T-opsem FCP on adopting at least a minimum set of Union Validity Rules. This would allow documenting all type validity invariants in the dynamic.layout spec chapter (spec#15).

Based on discussions on zulip (https://rust-lang.zulipchat.com/#narrow/stream/136281-t-opsem/topic/Can.20we.20decide.20the.20validity.20invariant.20of.20unions.3F) the proposed rule is (in prose)

A value of a union type is valid if each value byte it was computed from was either initialized, or in at least one field of the union, that byte of that field is either a padding byte, or valid when computed from an uninitialized value.

The term "value byte" is used in the above chapter to mean "Any byte that is not a padding byte". Notably, any byte that is padding in all fields is padding in the union, and thus always allowed to be uninit.

The minimum rules ensure we can widen the Validity Invariant in the future to something closer to (or exactly) a trivial validity invariant.

[chorman0773]

@rustbot label +A-unions +A-validity +T-opsem

[chorman0773]

I'm not sure whether I should also add S-pending-team-decision.

[Lokathor]

I don't wanna pick on your wording too closely because it's a draft and all, but I think I know what you're trying to say, and I can barely tell what that means.

[chorman0773]

Do you have a suggestion for better wording?

[Lokathor]

I think what's giving me trouble is that it's all one sentence with too many little parts in the sentence. Also, the use of the past tense strikes me as a little odd, though maybe it fits in the larger context. Also, it doesn't matter why a byte can be uninit, just that it can be for whatever reason. Keep things simple by not trying to list particular reasons.

Try this on for size:

A value of a union type is valid if each value byte is one of:

• initialized
• uninitialized and at least one field of the union is also allowed to be uninitialized at the same byte position

[chorman0773]

The issue is that the way the rest of the chapter is I think makes it ill-defined to ask about the validity invariants of a padding byte. Validity checking is spec'd after value computation (and talks about the actual value), and padding bytes are completely ignored.

[Lokathor]

what? Then change the rest of the chapter, I guess.

If a spec can't tell me, very plainly, which bytes within a type must be initialized or not... well then something is very wrong with the organization of that spec.

You could say "padding bytes are valid when initialized and when uninitialized" somewhere, and that seems sufficient explanation.

[chorman0773]

If a spec can't tell me, very plainly, which bytes within a type must be initialized or not... well then something is very wrong with the organization of that spec.

The spec tells you when a given value is valid. Parts of the chapter (IE. validity for scalar types), say

A value of is valid when all bytes the value was computed from are initialized.

Talking about validity in terms of individual bytes is actually ill-defined IMO, because validity is a compound property of a whole value (NonZeroU32 doesn't forbid any particular byte from being 0). So the chapter is written with that fact in mind. It follows that padding bytes, which don't participate in determining the value of a type, can be any value - initialized or not.

[Lokathor]

I'm not talking about which specific initialized values each byte can be though. Needing to be initialized or not is an "earlier" property than needing to pick a specific value. All four bytes in NonZeroU32 need to be initialized, and we can state this about every byte or not. As far as I know, we can state the initialization requirements of all bytes in all types, actually.

[CAD97]

I think that {initialized INCLUSIVE-OR byte can be uninitialized/padding in at least one variant} being sufficient validity should be fairly non-controversial¹, and support an FCP canonicalizing such². I don't know exactly how the draft spec is handling provenance, but the FCP should explicitly acknowledge it (we've got T-lang FCP accepted that provenance exists, IIRC) even if to only say that nothing is determined yet.

Minor side notes:

• Since #[repr(Rust)] unions do not specify layout (variant offsets), this spec has no implications at the repr-generic level, but only at the levels after instantiating with a specific layout choice.
• To maintain ABI transparency, it may be required that union padding can get reset when manipulated by-value (at least for non-#[repr(Rust)] unions).

Footnotes

1. Although not a given, since "untagged enum" representation wants stronger validity that preserves niche availability. ↩

2. Provided the FCP has a local copy of the disclaimer that while sufficient, it may be relaxed and not be required, thus is not a guarantee that unsafe may soundly expect from arbitrary code. ↩

[chorman0773]

The spec chapter is quite clear the repr(Rust) unions don't have defined offsets for each field. In general, I did my best to encapsilate only what guarantees currently exist while being complete. Unions were the only place I was unable to do that.

[chorman0773]

A value of a union type is valid if each value byte is one of:

• initialized
• uninitialized and at least one field of the union is either not a value byte in that field or is allowed to be uninitialized at the corresponding offset