Bob.Build.PhysicalComponents

1module Bob.Build.PhysicalComponents
2
3import Accelerator.SM86.InstructionEncoding
4import Bob.ArenaPlan
5import Bob.Build.SM86Programs
6import Bob.Learner
7import Bob.Model
8import Bob.TrainingRun
9import Compiler.Planning.VA
10import Data.Bytes
11import Float32Exact
12import BinaryFloatModel
13import Float32Model
14import FloatLiteralSpec
15import Hardware.Nvidia.SM86.Command.QMD
16import Hardware.Nvidia.SM86.Command.WholeProgramPlan
17import Model.Config
18import Model.Parameter
19import Model.Word64
20import Runtime.ArenaCertificate
21import Runtime.DeviceArenaCertificate
22import Platform.Linux.Nvidia.PlanHost
23import Platform.Linux.Nvidia.PlanHostRequest
24import Realization.Nvidia.SM86.AdamWSM86
25import Realization.Nvidia.SM86.EmbeddingGatherF32SM86
26import Realization.Nvidia.SM86.GreedyArgmaxSM86
27import Std.Natural
28
29-- Bob declares what runs on the device: four typed regions, the launches that
30-- use them with their kernel parameters, and the order they are submitted in.
31-- The NVIDIA backend places and prunes the regions, places the parameter
32-- blocks, and encodes the QMD table, pushbuffer and GPFIFO from this plan.
33-- Nothing here joins bytes or knows where anything lands.
34
35-- Bob's four device kernels, each encoded by its maintained owner.
36def bobGatherMachineBytes : Bytes =
37  (eliminate
38    EmbeddingGatherF32ImageResult
39    (lambda unrestricted current : (family EmbeddingGatherF32ImageResult) . Bytes)
40    bobPredictionRowImage
41    (branch EmbeddingGatherF32ImageReady image digest telemetry . image)
42    (branch EmbeddingGatherF32ImageFailed error ordinal detail telemetry . b""))
43
44def bobLossMachineBytes : Bytes =
45  (eliminate
46    SM86ProgramEncodingResult
47    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
48    bobLossGradientImage
49    (branch SM86ProgramEncodingSucceeded image telemetry . image)
50    (branch SM86ProgramEncodingFailed ordinal failure telemetry . b""))
51
52def bobAdamMachineBytes : Bytes =
53  (eliminate
54    AdamWF32SM86ImageResult
55    (lambda unrestricted current : (family AdamWF32SM86ImageResult) . Bytes)
56    bobOptimizerImage
57    (branch AdamWF32SM86ImageReady image digest encoding identity telemetry . image)
58    (branch AdamWF32SM86ImageFailed error ordinal detail telemetry . b""))
59
60def bobArgmaxMachineBytes : Bytes =
61  (eliminate
62    SM86ProgramEncodingResult
63    (lambda unrestricted current : (family SM86ProgramEncodingResult) . Bytes)
64    (sm86EncodeProgram greedyArgmaxSM86ByteVocabularyProgram)
65    (branch SM86ProgramEncodingSucceeded image telemetry . image)
66    (branch SM86ProgramEncodingFailed ordinal failure telemetry . b""))
67
68def bobWord64 =
69  (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))
70
71-- Device regions.  Registers, block width and shared memory are properties of
72-- each kernel; the backend derives the QMD resource fields from them.
73def bobRegion =
74  (lambda unrestricted identity : Bytes .
75    (lambda unrestricted material : Bytes .
76      (lambda unrestricted registers : Nat .
77        (lambda unrestricted blockX : Nat .
78          (constructor NvidiaDeviceRegion NvidiaDeviceRegionValue
79            identity material registers blockX zero)))))
80
81def bobRegions : (family NvidiaDeviceRegions) =
82  (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext
83    (bobRegion b"bob-row-gather" bobGatherMachineBytes 24 64)
84    (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext
85      (bobRegion b"bob-loss-gradient" bobLossMachineBytes 32 256)
86      (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext
87        (bobRegion b"bob-adamw" bobAdamMachineBytes 32 256)
88        (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext
89          (bobRegion b"bob-greedy-argmax" bobArgmaxMachineBytes 32 1)
90          (constructor NvidiaDeviceRegions NvidiaDeviceRegionsEnd)))))
91
92-- A launch names its region by the region's place in the declared order.  The
93-- places follow from the region sizes and the plan's alignment; the backend
94-- uses them only as keys and repacks whatever survives.
95def bobRegionAlignment : Nat =
96  256
97
98def bobAlign =
99  (lambda unrestricted value : Nat .
100    (naturalMultiply
101      (naturalDivideUnchecked
102        (naturalAdd value (naturalSaturatingSubtract bobRegionAlignment 1))
103        bobRegionAlignment)
104      bobRegionAlignment))
105
106def bobGatherPlace : Nat =
107  zero
108
109def bobLossPlace : Nat =
110  (bobAlign (naturalAdd bobGatherPlace (bytes-length bobGatherMachineBytes)))
111
112def bobAdamPlace : Nat =
113  (bobAlign (naturalAdd bobLossPlace (bytes-length bobLossMachineBytes)))
114
115def bobArgmaxPlace : Nat =
116  (bobAlign (naturalAdd bobAdamPlace (bytes-length bobAdamMachineBytes)))
117
118def bobCodeExtent : Nat =
119  (bobAlign (naturalAdd bobArgmaxPlace (bytes-length bobArgmaxMachineBytes)))
120
121def bobParameterBytes : Nat =
122  512
123
124def bobKernel =
125  (lambda unrestricted place : Nat .
126    (lambda unrestricted gridX : Nat .
127      (constructor NvidiaLaunchKernel NvidiaLaunchKernelValue
128        (bobWord64 (naturalAdd bobProgramBase place))
129        gridX 1 1 1 1 bobParameterBytes)))
130
131-- Kernel parameters are sparse 8-byte words in a 512-byte constant buffer.
132-- Every Bob kernel reads its arguments from the SM86 parameter base on: the
133-- i-th argument is word `bobArgument i`; a kernel's binary32 scalars follow
134-- its pointers, two to a word (the loss kernel's after six pointer slots,
135-- AdamW's after its four).
136def bobArgument =
137  (lambda unrestricted i : Nat . (naturalAdd (naturalDivideUnchecked qmdKernelParameterBase 8) i))
138
139def bobNoPatches : (family NvidiaParameterPatches) =
140  (constructor NvidiaParameterPatches NvidiaParameterPatchesEnd)
141
142def bobPatch =
143  (lambda unrestricted word : Nat .
144    (lambda unrestricted value : (family ModelWord64) .
145      (lambda unrestricted rest : (family NvidiaParameterPatches) .
146        (constructor NvidiaParameterPatches NvidiaParameterPatchesNext
147          (constructor NvidiaParameterPatch NvidiaParameterPatchValue word value)
148          rest))))
149
150-- Consecutive words taken from little-endian bytes, used for the f32 scalars a
151-- kernel reads after its addresses.
152def bobWordPatches =
153  (lambda unrestricted words : Nat .
154    (nat-eliminate
155      (lambda unrestricted current : Nat .
156        (pi unrestricted word : Nat .
157          (pi unrestricted input : Bytes .
158            (pi unrestricted rest : (family NvidiaParameterPatches) .
159              (family NvidiaParameterPatches)))))
160      (lambda unrestricted word : Nat .
161        (lambda unrestricted input : Bytes .
162          (lambda unrestricted rest : (family NvidiaParameterPatches) . rest)))
163      (lambda unrestricted predecessor : Nat .
164        (lambda unrestricted induction :
165          (pi unrestricted word : Nat .
166            (pi unrestricted input : Bytes .
167              (pi unrestricted rest : (family NvidiaParameterPatches) .
168                (family NvidiaParameterPatches)))) .
169          (lambda unrestricted word : Nat .
170            (lambda unrestricted input : Bytes .
171              (lambda unrestricted rest : (family NvidiaParameterPatches) .
172                (eliminate
173                  DataBytesWord64DecodeResult
174                  (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
175                    (family NvidiaParameterPatches))
176                  (dataBytesReadWord64LE input)
177                  (branch DataBytesWord64Decoded value remaining .
178                    (bobPatch word value (induction (succ word) remaining rest)))
179                  (branch DataBytesWord64DecodeFailed error . rest)))))))
180      words))
181
182def bobBlock =
183  (lambda unrestricted patches : (family NvidiaParameterPatches) .
184    (constructor NvidiaParameterBlock NvidiaParameterBlockValue patches))
185
186-- Bob's device arena: one system-memory staging buffer the host maps, each
187-- tensor after the previous, page-aligned: the parameters and the two
188-- optimizer moments (the checkpoint, contiguous, in that order), the
189-- gradients, the input record (Bob.TrainingRun), the two loss blocks, the
190-- prompts' logit rows and their predictions.  The host (Bob.Build.NativeHost)
191-- reads the input record and the checkpoint into it and writes the results
192-- out of it.
193def bobArenaNext =
194  (lambda unrestricted address : Nat .
195    (lambda unrestricted bytes : Nat . (vaPlaceAfter address bytes nvidiaPlanHostPageBytes)))
196def bobTableBytes : Nat = (naturalMultiply bobCheckpointBytesPerScalar bobParameterCount)
197def bobRowBytes : Nat = (naturalMultiply bobCheckpointBytesPerScalar bobVocabularySize)
198-- a loss block: one binary32 per row
199def bobLossBytes : Nat = bobRowBytes
200def bobLogitRowsBytes : Nat = (naturalMultiply bobPromptCount bobRowBytes)
201def bobPredictionsBytes : Nat = (naturalMultiply bobPromptCount bobPredictionBytes)
202def bobParametersAddress : Nat = bobArenaBase
203def bobFirstMomentAddress : Nat = (bobArenaNext bobParametersAddress bobTableBytes)
204def bobSecondMomentAddress : Nat = (bobArenaNext bobFirstMomentAddress bobTableBytes)
205def bobGradientsAddress : Nat = (bobArenaNext bobSecondMomentAddress bobTableBytes)
206def bobInputAddress : Nat = (bobArenaNext bobGradientsAddress bobTableBytes)
207def bobTargetsAddress : Nat = (naturalAdd bobInputAddress bobInputTargetsOffset)
208def bobPromptBytesAddress : Nat = (naturalAdd bobInputAddress bobInputPromptsOffset)
209def bobInitialLossAddress : Nat = (bobArenaNext bobInputAddress bobInputRecordBytes)
210def bobTrainingLossAddress : Nat = (bobArenaNext bobInitialLossAddress bobLossBytes)
211def bobLogitRowsAddress : Nat = (bobArenaNext bobTrainingLossAddress bobLossBytes)
212def bobPredictionsAddress : Nat = (bobArenaNext bobLogitRowsAddress bobLogitRowsBytes)
213def bobArenaBytes : Nat =
214  (naturalSaturatingSubtract (naturalAdd bobPredictionsAddress bobPredictionsBytes) bobParametersAddress)
215-- the result record: the initial loss block, the training loss block, the
216-- logit rows
217def bobResultInitialLossOffset : Nat = 0
218def bobResultTrainingLossOffset : Nat = bobLossBytes
219def bobResultLogitRowsOffset : Nat = (naturalMultiply 2 bobLossBytes)
220
221-- log2 e, ln 2 and 1 / 256 as binary32. BigramLossGradientSM86 converts
222-- the log2 reduction back to natural logarithms for each row's cross entropy;
223-- inverse rows scales the gradients, not the stored row losses. The row
224-- block must be reduced separately before reporting a mean objective. Each
225-- constant is held to its exact value (Float32Exact).
226def bobInverseRows : Nat = 0x3b800000
227
228def bobInverseRowsDerived :
229  (equal Nat bobInverseRows (float32ExactRational 1 bobVocabularySize)) =
230  (refl Nat bobInverseRows)
231
232def bobWordPair =
233  (lambda unrestricted low : Nat .
234    (lambda unrestricted high : Nat . (naturalAdd low (naturalMultiply high 4294967296))))
235
236def bobLossBlock =
237  (lambda unrestricted lossAddress : Nat .
238    (bobBlock
239      (bobPatch (bobArgument 0) (bobWord64 bobParametersAddress)
240        (bobPatch (bobArgument 1) (bobWord64 bobGradientsAddress)
241          (bobPatch (bobArgument 2) (bobWord64 bobTargetsAddress)
242            (bobPatch (bobArgument 3) (bobWord64 lossAddress)
243              (bobPatch (bobArgument 6) (bobWord64 (bobWordPair float32Log2E float32Ln2))
244                (bobPatch (bobArgument 7) (bobWord64 (bobWordPair bobInverseRows 0)) bobNoPatches))))))))
245
246def bobGatherBlock =
247  (lambda unrestricted index : Nat .
248    (bobBlock
249      (bobPatch (bobArgument 0) (bobWord64 (naturalAdd bobLogitRowsAddress (naturalMultiply index bobRowBytes)))
250        (bobPatch (bobArgument 1) (bobWord64 (naturalAdd bobPromptBytesAddress (naturalMultiply index bobInputWordBytes)))
251          (bobPatch (bobArgument 2) (bobWord64 bobParametersAddress) bobNoPatches)))))
252
253def bobArgmaxBlock =
254  (lambda unrestricted index : Nat .
255    (bobBlock
256      (bobPatch (bobArgument 0) (bobWord64 (naturalAdd bobPredictionsAddress (naturalMultiply index bobPredictionBytes)))
257        (bobPatch (bobArgument 1) (bobWord64 (naturalAdd bobLogitRowsAddress (naturalMultiply index bobRowBytes)))
258          bobNoPatches))))
259
260-- AdamW's nine f32 scalars for one step, read after its four addresses.
261def bobAdamBlock =
262  (lambda unrestricted scalars : Bytes .
263    (bobBlock
264      (bobPatch (bobArgument 0) (bobWord64 bobParametersAddress)
265        (bobPatch (bobArgument 1) (bobWord64 bobGradientsAddress)
266          (bobPatch (bobArgument 2) (bobWord64 bobFirstMomentAddress)
267            (bobPatch (bobArgument 3) (bobWord64 bobSecondMomentAddress)
268              (bobWordPatches 5 (bobArgument 4) (bytes-append scalars b"\x00\x00\x00\x00") bobNoPatches)))))))
269
270def bobLaunch =
271  (lambda unrestricted identity : Bytes .
272    (lambda unrestricted kernel : (family NvidiaLaunchKernel) .
273      (lambda unrestricted block : (family NvidiaParameterBlock) .
274        (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleOne
275          (constructor NvidiaLaunchTemplate NvidiaLaunchTemplateValue identity kernel block)))))
276
277def bobThen =
278  (lambda unrestricted left : (family NvidiaLaunchSchedule) .
279    (lambda unrestricted right : (family NvidiaLaunchSchedule) .
280      (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleAppend left right)))
281
282def bobLossLaunch =
283  (lambda unrestricted lossAddress : Nat .
284    (bobLaunch b"bob-loss-gradient" (bobKernel bobLossPlace 1) (bobLossBlock lossAddress)))
285
286-- Predicting one prompt gathers its logits row and takes the greedy argmax.
287def bobPredictLaunches =
288  (lambda unrestricted index : Nat .
289    (bobThen
290      (bobLaunch b"bob-row-gather" (bobKernel bobGatherPlace 1) (bobGatherBlock index))
291      (bobLaunch b"bob-greedy-argmax" (bobKernel bobArgmaxPlace 1) (bobArgmaxBlock index))))
292
293-- One training step updates the table from the current gradients and then
294-- evaluates the loss and the next gradients.
295def bobTrainingStep =
296  (lambda unrestricted scalars : Bytes .
297    (bobThen
298      (bobLaunch b"bob-adamw" (bobKernel bobAdamPlace 256) (bobAdamBlock scalars))
299      (bobLossLaunch bobTrainingLossAddress)))
300
301def bobTrainingSteps : Nat =
302  bobUpdatesPerInvocation
303
304-- Steps 1 .. count, in order, each with its own scalars.
305def bobTrainingSchedule =
306  (lambda unrestricted count : Nat .
307    (nat-eliminate
308      (lambda unrestricted current : Nat . (family NvidiaLaunchSchedule))
309      (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleEmpty)
310      (lambda unrestricted predecessor : Nat .
311        (lambda unrestricted induction : (family NvidiaLaunchSchedule) .
312          (bobThen induction (bobTrainingStep (bobAdamStepScalars (succ predecessor))))))
313      count))
314
315-- Prompts 0 .. count - 1, in order.
316def bobPredictionSchedule : (family NvidiaLaunchSchedule) =
317  (nat-eliminate
318    (lambda unrestricted current : Nat . (family NvidiaLaunchSchedule))
319    (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleEmpty)
320    (lambda unrestricted predecessor : Nat .
321      (lambda unrestricted induction : (family NvidiaLaunchSchedule) .
322        (bobThen induction (bobPredictLaunches predecessor))))
323    bobPromptCount)
324
325def bobInitialLoss : (family NvidiaLaunchSchedule) =
326  (bobLossLaunch bobInitialLossAddress)
327
328-- the forward launches: the initial loss and the prompts' predictions,
329-- before the request's operation decides whether training follows
330def bobForwardSchedule : (family NvidiaLaunchSchedule) =
331  (bobThen bobInitialLoss bobPredictionSchedule)
332
333def bobLaunchSchedule : (family NvidiaLaunchSchedule) =
334  (bobThen bobForwardSchedule (bobTrainingSchedule bobTrainingSteps))
335
336def bobForwardLaunches : Nat = (nvidiaLaunchScheduleCount bobForwardSchedule)
337
338-- the launch of update k's AdamW (from 0; first in its step): after the
339-- forward launches, the earlier steps'.  The host writes each update's
340-- step size and epsilon into its parameter block
341-- (Platform.Linux.Nvidia.PlanHostAdamW); the values baked here are the
342-- first invocation's.
343def bobStepLaunches : Nat =
344  (nvidiaLaunchScheduleCount (bobTrainingStep (bobAdamStepScalars 1)))
345
346def bobAdamWLaunch =
347  (lambda unrestricted k : Nat . (naturalAdd bobForwardLaunches (naturalMultiply k bobStepLaunches)))
348def bobLaunchCount : Nat = (nvidiaLaunchScheduleCount bobLaunchSchedule)
349
350-- Each launch is submitted alone.  The run submits every launch once, in
351-- order, and then predicts again from the trained table.
352def bobSubmitEach =
353  (lambda unrestricted count : Nat .
354    (lambda unrestricted firstLaunch : Nat .
355      (lambda unrestricted firstSemaphore : Nat .
356        (constructor NvidiaSubmissionSchedule NvidiaSubmissionScheduleRepeat
357          count 1 prSemaphoreStride
358          (constructor NvidiaSubmissionSchedule NvidiaSubmissionScheduleOne
359            (constructor NvidiaSubmissionBatch NvidiaSubmissionBatchValue
360              b"bob-submission"
361              firstSemaphore
362              (constructor NvidiaLaunchReferences NvidiaLaunchReferencesRange firstLaunch 1)))))))
363
364def bobPredictionLaunches : Nat =
365  (nvidiaLaunchScheduleCount bobPredictionSchedule)
366
367def bobSubmissionSchedule : (family NvidiaSubmissionSchedule) =
368  (constructor NvidiaSubmissionSchedule NvidiaSubmissionScheduleAppend
369    (bobSubmitEach bobLaunchCount zero zero)
370    (bobSubmitEach bobPredictionLaunches (nvidiaLaunchScheduleCount bobInitialLoss) (naturalMultiply bobLaunchCount prSemaphoreStride)))
371
372def bobSubmissionCount : Nat =
373  (naturalAdd bobLaunchCount bobPredictionLaunches)
374
375-- The program component is exactly the retained code and one parameter block
376-- per launch; the QMD table is one 256-byte record per launch.
377def bobProgramBytes : Nat =
378  (naturalAdd bobCodeExtent (naturalMultiply bobLaunchCount bobParameterBytes))
379
380def bobQMDTableBytes : Nat =
381  (naturalMultiply bobLaunchCount qmdRecordBytes)
382
383def bobWholeProgramPlan =
384  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
385    (lambda unrestricted architecture : (family ModelWord32) .
386      (lambda unrestricted computeClass : (family ModelWord32) .
387        (lambda unrestricted spaVersion : (family ModelWord32) .
388          (constructor
389            NvidiaWholeProgramPlan
390            NvidiaWholeProgramPlanValue
391            component
392            architecture
393            computeClass
394            spaVersion
395            (bobWord64 bobProgramBase)
396            (bobWord64 bobQMDBase)
397            (bobWord64 bobPushbufferBase)
398            (bobWord64 bobSemaphoreBase)
399            bobRegionAlignment
400            bobProgramBytes
401            bobRegions
402            bobLaunchSchedule
403            bobLaunchCount
404            bobQMDTableBytes
405            bobSubmissionSchedule
406            bobSubmissionCount
407            bobSubmissionCount)))))
408
409def bobPhysicalComponent =
410  (lambda unrestricted component : (family NvidiaWholeProgramComponent) .
411    (lambda unrestricted architecture : (family ModelWord32) .
412      (lambda unrestricted computeClass : (family ModelWord32) .
413        (lambda unrestricted spaVersion : (family ModelWord32) .
414          (compiler-native-encode
415            (family NvidiaWholeProgramPlan)
416            (bobWholeProgramPlan component architecture computeClass spaVersion))))))
417
418-- ---- the device side of the arena ----
419-- Every tensor Bob places lives for the whole program (the arena above);
420-- each launch's identity is its phase.  Runtime.DeviceArenaCertificate
421-- decides that the tensors are disjoint and that every pointer a launch
422-- passes lies in one of them; the host is admitted only then
423-- (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)))))
432
433def bobNoPlanes : (family ArenaResidents) =
434  (constructor ArenaResidents ArenaResidentsEnd)
435
436def bobDeviceWindows : (family ArenaResidents) =
437  (bobPlane b"arena" bobParametersAddress bobArenaBytes bobNoPlanes)
438
439def bobDeviceGlobals : (family ArenaResidents) =
440  (bobPlane b"parameters" bobParametersAddress bobTableBytes
441    (bobPlane b"first-moments" bobFirstMomentAddress bobTableBytes
442      (bobPlane b"second-moments" bobSecondMomentAddress bobTableBytes
443        (bobPlane b"gradients" bobGradientsAddress bobTableBytes
444          (bobPlane b"input-record" bobInputAddress bobInputRecordBytes
445            (bobPlane b"initial-loss" bobInitialLossAddress bobLossBytes
446              (bobPlane b"training-loss" bobTrainingLossAddress bobLossBytes
447                (bobPlane b"logit-rows" bobLogitRowsAddress bobLogitRowsBytes
448                  (bobPlane b"predictions" bobPredictionsAddress bobPredictionsBytes bobNoPlanes)))))))))
449
450def bobPhase =
451  (lambda unrestricted identity : Bytes .
452    (lambda unrestricted rest : (family DeviceArenaPhases) .
453      (constructor DeviceArenaPhases DeviceArenaPhasesNext
454        (constructor DeviceArenaPhase DeviceArenaPhaseValue identity bobNoPlanes bobNoPlanes)
455        rest)))
456
457def bobDevicePhases : (family DeviceArenaPhases) =
458  (bobPhase b"bob-loss-gradient"
459    (bobPhase b"bob-row-gather"
460      (bobPhase b"bob-greedy-argmax"
461        (bobPhase b"bob-adamw" (constructor DeviceArenaPhases DeviceArenaPhasesEnd)))))
462
463-- 0 when the device side is certified; a function, so a build computes it
464-- only where it is applied
465def bobDeviceHazardOf =
466  (lambda unrestricted ignored : Nat .
467    (deviceArenaHazard bobDeviceWindows bobDeviceGlobals bobDevicePhases bobLaunchSchedule bobSubmissionSchedule))
468
469def bobDeviceHazard : Nat =
470  (bobDeviceHazardOf zero)