Check input cases and union members

RFC 0025 rechecks helpers under bounded facts established by a caller, including read-only helpers. For example, read_if(0, 0) can be checked when read_if returns immediately for a zero selector, even if its other branch has unresolved arithmetic or memory accesses. Forwarding helpers and resolved callbacks retain the case premises. Every evaluated selector still needs initialized storage; a tag value supplies no payload or pointee permission.

Named, complete unions with scalar or pointer members can be checked directly:

union value { int number; int *pointer; };
int main(void) {
    int n = 7;
    union value v = {.pointer = &n};
    return *v.pointer;
}

Reading a member requires evidence that this member was initialized. Reading another member, or changing an enclosing tag without establishing the selected payload, leaves checking incomplete. A pointer member independently needs live storage, sufficient bounds and initialized pointee bytes. Compatible complete record copies preserve member evidence; partial byte writes and unknown writes invalidate overlapping values. Guarded branch joins retain only evidence justified on every applicable incoming path.

A helper can require an input member or establish a member through an output parameter or a returned record. The union-member requirement is separate from initialized byte ranges. Unsupported aggregate/array members, anonymous member promotion, bit-fields, volatile/atomic union storage and representation punning remain incomplete. There is no union or tag annotation.