Bob.Build.PhysicalComponents

---- the device side of the arena ---- Every tensor Bob places lives for the whole program (the arena above); each launch's identity is its phase. Runtime.DeviceArenaCertificate decides that the tensors are disjoint and that every pointer a launch passes lies in one of them; the host is admitted only then (Bob.Build.NativeHost).

424def bobPlane =
425  (lambda unrestricted name : Bytes .
426    (lambda unrestricted address : Nat .
427      (lambda unrestricted bytes : Nat .
428        (lambda unrestricted rest : (family ArenaResidents) .
429          (constructor ArenaResidents ArenaResidentsNext
430            (constructor ArenaResident ArenaResidentValue name address bytes bobRegionAlignment)
431            rest)))))