Runtime.ArenaCertificate

---- the schedule over the arena ---- What the certificate sees of a host's schedule over its host-visible arena: the host writes a range, reads a range, awaits a submission by its generation (the submissions issued once it is written; the host goes on only when that one has completed), or observes an awaited submission (a timestamp of it). The device's work is ordered with the host's by those waits alone, so the certificate decides that the order the host relies on is the order it has: * generations strictly increase, so every wait awaits work its own submit issued -- a completion of an earlier generation cannot satisfy it -- and the last is the plan's count: every submission awaited; * a host write is pending until a submission consumes it; a host write over a pending range would overwrite staging no submission has read, and none may be pending at the end; * a host read of a pending range would read back the host's own staging, not a submission's result; * an observation names an awaited generation. Ranges of no bytes touch nothing.

127def arenaRangesNone : (family ArenaRanges) = (constructor ArenaRanges ArenaRangesNone)