Coppelius.Build.Graph

---- the device side of the arena ---- Every tensor the plan places, named: the globals, live for the whole program, and each phase's planes (fresh, or carried from an earlier phase). Runtime.DeviceArenaCertificate decides, on the launch and submission schedules above, that every pointer a launch passes lies in a plane of its phase or in a global, that the planes live together never share a byte, and that no carried plane is overwritten before its phase runs; the host is admitted only then (Coppelius.Build.NativeHost). Staging planes are declared fresh: the host writes them between submissions, in the order the host side of the certificate decides.

3047def cgPlane =
3048  (lambda unrestricted name : Bytes .
3049    (lambda unrestricted address : Nat .
3050      (lambda unrestricted bytes : Nat .
3051        (constructor ArenaResident ArenaResidentValue name address bytes cgParameterAlignment))))