Runtime.ArenaCertificate

A placement certificate for a static arena: not a byte total but the actual placement. Every resident names its offset, extent and alignment; the certificate holds when each resident is aligned, non-empty and inside the arena, and every pair of residents is disjoint. Residents here are all live for the whole program, so disjointness is the whole aliasing rule; lifetimes and happens-before come later, with the event graph. The checker decides the certificate on a concrete plan by normalization.

18field unrestricted arenaResidentAlignment : Nat