Minimum guarantees for union construction and typed copies?

[joshlf]

Given #438 (comment), zerocopy is interested in exploring alternative routes to supporting union transmutations. Our current thinking is that we can accomplish this via safety rather than bit validity requirements.

In order to do this, we'd need two things guaranteed from the language. My question is: Are we comfortable guaranteeing these two invariants?

Safe union construction

Given a union where every possible value of every field contains an initialized byte at a particular offset, we'd like it to be impossible for safe code to produce a value of that union which has an uninitialized byte at that byte offset. It would be acceptable for unsafe code to be able to produce such a value.

Typed union copies

We'd like to guarantee that, in a typed copy of a union value, the byte at any byte position is preserved if that position is initialized in any valid value of any field type. This amounts to saying that the following code is guaranteed to be sound:

let t: T = ...;
let mu = MaybeUninint::<T>::new(t);
// SAFETY: This typed copy copies all of the initialized bytes in `t`, which is a valid `T`.
let t = unsafe { mu.assume_init() };

[RalfJung]

Generally the safety invariant of a union is almost entirely up to the user -- the language puts fairly few constraints on that since all union reads are unsafe.

Safe union construction

So for instance, this means we can never have a union constructor that safely builds a union without initializing one of its fields? That seems reasonable to me. However, this is more of a t-types/t-lang question.

We'd like to guarantee that, in a typed copy of a union value, the byte at any byte position is preserved if that position is initialized in any valid value of any field type. This amounts to saying that the following code is guaranteed to be sound:

The text and the example are saying quite different things here. The example just needs "if a union was created by initializing one of its fields, then a typed copy of the union will preserve the value of that field". That's completely obvious IMO, so obvious in fact that it is hard to even state (and we don't bother stating anything like that for structs or enums, either).

We can go a little further and say that every union value you can construct in safe code will be preserved by a typed copy.

However, the text talks about a per-byte property, which would kick in even when "mixing" different fields in more ways than is possible in safe code. I think we should guarantee that, but I also think unions should be bags of bytes without validity invariant -- and quite a few people disagree with the latter. The further we move away from "bag of bytes", the harder it becomes to make guarantees like this.