Bob.Build.PhysicalComponents

Bob's device arena: one system-memory staging buffer the host maps, each tensor after the previous, page-aligned: the parameters and the two optimizer moments (the checkpoint, contiguous, in that order), the gradients, the input record (Bob.TrainingRun), the two loss blocks, the prompts' logit rows and their predictions. The host (Bob.Build.NativeHost) reads the input record and the checkpoint into it and writes the results out of it.

193def bobArenaNext =
194  (lambda unrestricted address : Nat .
195    (lambda unrestricted bytes : Nat . (vaPlaceAfter address bytes nvidiaPlanHostPageBytes)))