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.
13family ArenaResident : Type 0
14constructor ArenaResidentValue
15field unrestricted arenaResidentIdentity : Bytes
16field unrestricted arenaResidentOffset : Nat
17field unrestricted arenaResidentExtent : Nat
18field unrestricted arenaResidentAlignment : NatThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.