1module Bob.Build.NativeHost
2
3import Bob.ArenaPlan
4import Bob.Build.PhysicalComponents
5import Bob.Learner
6import Bob.Model
7import Checkpoint.Envelope
8import Bob.TrainingRun
9import Data.Bytes
10import Data.Float32Bits
11import Data.JSON
12import Data.JSONAccess
13import Data.UTF8
14import Data.JSONRender
15import Model.Config
16import Model.Parameter
17import Model.Word64
18import Model.Word32
19import Observe.CapturePolicy
20import Observe.Interchange
21import Observe.Value
22import Observe.Metric
23import Runtime.NativeObservedProgram
24import Observe.Execution
25import Runtime.NativeTelemetry
26import Runtime.NativeTelemetryIdentity
27import Runtime.ArenaCertificate
28import Runtime.TelemetryValue
29import Runtime.TelemetryRecord
30import Runtime.TelemetryPolicy
31import Runtime.TelemetryDrain
32import Runtime.TelemetryCapture
33import Platform.Linux.Nvidia.Compatibility
34import Platform.Linux.Nvidia.PlanHost
35import Platform.Linux.Nvidia.PlanHostAdamW
36import Platform.Linux.Nvidia.PlanHostRequest
37import Platform.Linux.Nvidia.RequestCapture
38import Runtime.NativePhysicalEmbeddedArtifact
39import Realization.Nvidia.SM86.AdamWSM86
40import Runtime.NativePhysicalProgram
41import Std.Float
42import Std.List
43import Std.Natural
44
45-- what the realization reports of the parameter blocks: each launch's
46-- block's address, and the word at the AdamW step size's offset in it
47-- (Bob.Build.DirectArtifact passes them)
48family BobRealizedTables : Type 0
49constructor BobRealizedTablesValue
50field unrestricted bobRealizedParameterAddresses : Bytes
51field unrestricted bobRealizedStepWords : Bytes
52
53end-family
54
55-- Values are taken from the semantics that also construct the executable.
56-- These describe its available training policy, not completed updates, restored
57-- state, input contents or facts about the device on which it eventually runs.
58def bobNativeExecutionConfiguration : (family AosValue) =
59 (constructor
60 AosValue
61 AosMap
62 (constructor
63 AosValue
64 AosMembersNext
65 b"model"
66 (constructor
67 AosValue
68 AosMap
69 (constructor
70 AosValue
71 AosMembersNext
72 b"input"
73 (constructor AosValue AosText (project BobModelSemantics bobModelInputIdentity bobModel))
74 (constructor
75 AosValue
76 AosMembersNext
77 b"vocabulary"
78 (constructor AosValue AosU64 bobVocabularySize)
79 (constructor
80 AosValue
81 AosMembersNext
82 b"context_length"
83 (constructor AosValue AosU64 bobContextLength)
84 (constructor
85 AosValue
86 AosMembersNext
87 b"parameter_count"
88 (constructor AosValue AosU64 bobParameterCount)
89 (constructor AosValue AosMembersEnd))))))
90 (constructor
91 AosValue
92 AosMembersNext
93 b"learning"
94 (constructor
95 AosValue
96 AosMap
97 (constructor
98 AosValue
99 AosMembersNext
100 b"objective"
101 (constructor AosValue AosText bobObjectiveIdentity)
102 (constructor
103 AosValue
104 AosMembersNext
105 b"learner"
106 (constructor AosValue AosText bobLearnerIdentity)
107 (constructor
108 AosValue
109 AosMembersNext
110 b"learning_rate"
111 (constructor
112 AosValue
113 AosF32
114 (dataBytesRenderHex (dataFloat32EncodeBE bobLearningRate)))
115 (constructor
116 AosValue
117 AosMembersNext
118 b"first_moment_decay"
119 (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobBeta1)))
120 (constructor
121 AosValue
122 AosMembersNext
123 b"second_moment_decay"
124 (constructor
125 AosValue
126 AosF32
127 (dataBytesRenderHex (dataFloat32EncodeBE bobBeta2)))
128 (constructor
129 AosValue
130 AosMembersNext
131 b"epsilon"
132 (constructor
133 AosValue
134 AosF32
135 (dataBytesRenderHex (dataFloat32EncodeBE bobEpsilon)))
136 (constructor
137 AosValue
138 AosMembersNext
139 b"weight_decay"
140 (constructor
141 AosValue
142 AosF32
143 (dataBytesRenderHex (dataFloat32EncodeBE bobWeightDecay)))
144 (constructor AosValue AosMembersEnd)))))))))
145 (constructor
146 AosValue
147 AosMembersNext
148 b"run_policy"
149 (constructor
150 AosValue
151 AosMap
152 (constructor
153 AosValue
154 AosMembersNext
155 b"updates_per_training_invocation"
156 (constructor AosValue AosU64 bobUpdatesPerInvocation)
157 (constructor
158 AosValue
159 AosMembersNext
160 b"initialization"
161 (constructor
162 AosValue
163 AosText
164 (project
165 BobTrainingRunSemantics
166 bobRunDeterministicInitializationIdentity
167 bobTrainingRunSemantics))
168 (constructor
169 AosValue
170 AosMembersNext
171 b"input_record_bytes"
172 (constructor AosValue AosU64 bobInputRecordBytes)
173 (constructor
174 AosValue
175 AosMembersNext
176 b"native_only_required"
177 (constructor
178 AosValue
179 AosBool
180 (project
181 BobTrainingRunSemantics
182 bobRunNativeOnlyRequired
183 bobTrainingRunSemantics))
184 (constructor
185 AosValue
186 AosMembersNext
187 b"allowed_host_fallbacks"
188 (constructor
189 AosValue
190 AosU64
191 (project
192 BobTrainingRunSemantics
193 bobRunAllowedHostFallbacks
194 bobTrainingRunSemantics))
195 (constructor AosValue AosMembersEnd)))))))
196 (constructor
197 AosValue
198 AosMembersNext
199 b"checkpoint"
200 (constructor
201 AosValue
202 AosMap
203 (constructor
204 AosValue
205 AosMembersNext
206 b"schema"
207 (constructor
208 AosValue
209 AosText
210 (project
211 BobCheckpointTransportSchema
212 bobCheckpointSchemaIdentity
213 bobCheckpointSchema))
214 (constructor
215 AosValue
216 AosMembersNext
217 b"ordering"
218 (constructor
219 AosValue
220 AosText
221 (project
222 BobCheckpointTransportSchema
223 bobCheckpointOrderingIdentity
224 bobCheckpointSchema))
225 (constructor
226 AosValue
227 AosMembersNext
228 b"payload_bytes"
229 (constructor
230 AosValue
231 AosU64
232 (checkpointEnvelopeContractPayload bobCheckpointContract))
233 (constructor
234 AosValue
235 AosMembersNext
236 b"planes"
237 (constructor AosValue AosU64 bobCheckpointPlaneCount)
238 (constructor
239 AosValue
240 AosMembersNext
241 b"bytes_per_scalar"
242 (constructor AosValue AosU64 bobCheckpointBytesPerScalar)
243 (constructor AosValue AosMembersEnd)))))))
244 (constructor AosValue AosMembersEnd))))))
245
246-- This is a source declaration of the workload, not a claim that a run
247-- trained successfully. The frame binds its fresh run identity at import.
248-- One explicitly selected row, not a full-objective estimate. All numeric
249-- payload values are copied from the existing retired readback.
250def bobNativeRowDeclaration =
251 (lambda unrestricted stage : Bytes .
252 (constructor
253 TelemetryRecordDeclaration
254 TelemetryRecordDeclarationValue
255 b"alpha.learning.bob_row_loss@1"
256 b"metric"
257 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
258 b"direct"
259 b"native row zero loss copied from retired readback; one row sample"
260 (constructor
261 TelemetryCaptureValue
262 TelemetryMembersNext
263 b"row_loss"
264 (constructor TelemetryCaptureValue TelemetryFloat32 0)
265 (constructor
266 TelemetryCaptureValue
267 TelemetryMembersNext
268 b"completed_submissions"
269 (constructor TelemetryCaptureValue TelemetryUnsigned 1)
270 (constructor
271 TelemetryCaptureValue
272 TelemetryMembersNext
273 b"row_index"
274 (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosU64 0))
275 (constructor
276 TelemetryCaptureValue
277 TelemetryMembersNext
278 b"sample_count"
279 (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosU64 1))
280 (constructor
281 TelemetryCaptureValue
282 TelemetryMembersNext
283 b"stage"
284 (constructor
285 TelemetryCaptureValue
286 TelemetryConstant
287 (constructor AosValue AosText stage))
288 (constructor TelemetryCaptureValue TelemetryMembersEnd))))))))
289
290def bobNativeRowSchema =
291 (telemetryRecordJSON
292 (telemetryRecordSchemaJSON
293 (bobNativeRowDeclaration b"")
294 b"Native row-zero loss diagnostic"
295 (constructor
296 JSON
297 JSONObject
298 (aosField
299 b"row_loss"
300 (nvidiaRequestCaptureField b"f32")
301 (aosField
302 b"completed_submissions"
303 (nvidiaRequestCaptureField b"u64")
304 (aosField
305 b"row_index"
306 (nvidiaRequestCaptureField b"u64")
307 (aosField
308 b"sample_count"
309 (nvidiaRequestCaptureField b"u64")
310 (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd))))))))
311
312def bobNativeRowMeaning =
313 (telemetryRecordJSON
314 (aosSampledRowMetric
315 b"metric:alpha.learning.bob_row_loss@1:row_loss"
316 b"alpha.learning.bob_row_loss@1"
317 b"Native row-zero cross entropy"
318 b"nat/target-token"
319 b"row zero log(sum(exp(scores))) minus the target score; binary32 native result"
320 b"unbound"))
321
322def bobNativeRowTag0 : Nat =
323 (succ nvidiaRequestCaptureLastTag)
324
325def bobNativeRowTag1 : Nat =
326 (succ bobNativeRowTag0)
327
328def bobNativeCaptureSites =
329 (constructor
330 TelemetryPolicySites
331 TelemetryPolicySitesNext
332 bobNativeRowTag0
333 (constructor
334 CaptureSite
335 CaptureSiteValue
336 b"0000000000000000000000000000050b"
337 b"bob:before-training"
338 (constructor CaptureClass CaptureLifecycleClass)
339 1
340 2
341 1)
342 (bobNativeRowDeclaration b"before-training")
343 (constructor
344 TelemetryPolicySites
345 TelemetryPolicySitesNext
346 bobNativeRowTag1
347 (constructor
348 CaptureSite
349 CaptureSiteValue
350 b"0000000000000000000000000000050c"
351 b"bob:after-training"
352 (constructor CaptureClass CaptureLifecycleClass)
353 1
354 2
355 1)
356 (bobNativeRowDeclaration b"after-training")
357 nvidiaRequestCaptureSitesWithCheckpoint))
358
359def bobNativeRequestCapturePlan : (family TelemetryRoutedPolicyPlan) =
360 (compile-time
361 (nvidiaRequestCapturePlanWithSites
362 bobNativeCaptureSites
363 (constructor
364 StdList
365 StdListCons
366 Bytes
367 bobNativeRowSchema
368 (constructor
369 StdList
370 StdListCons
371 Bytes
372 bobNativeRowMeaning
373 (constructor
374 StdList
375 StdListCons
376 Bytes
377 (telemetryRecordJSON
378 (aosExecutionTemplate
379 b"execution-template:Bob.TrainingRun@1"
380 b"Bob"
381 b"learning"
382 b"alpha.systems"))
383 (constructor
384 StdList
385 StdListCons
386 Bytes
387 (telemetryRecordJSON
388 (aosExecutionConfiguration
389 b"configuration:Bob.TrainingRun@1"
390 bobNativeExecutionConfiguration))
391 (constructor StdList StdListEmpty Bytes)))))))
392
393-- Bob's host, derived from its plans by Platform.Linux.Nvidia.PlanHost: the
394-- UVM lifecycle with no video arena (every buffer is system memory), the
395-- four launch-table recipes expanded at startup, and the request schedule
396-- below -- the input record and the checkpoint staged, the forward
397-- launches (the initial loss and the three prompts' predictions) submitted
398-- one at a time, their results written, the request's operation, then the
399-- training steps and the predictions again, the results and the checkpoint
400-- written. Every number here is the physical components' or the training
401-- run's; the host addresses are this pairing's placement of its mappings
402-- in the process.
403-- ---- host placement (Bob.ArenaPlan places the mappings) ----
404-- buffer extents: the tables' bytes rounded to the mapping unit; the
405-- semaphores to a page; the GPFIFO with its USERD page after it
406def bobGPFIFOBufferBytes : Nat =
407 (naturalAdd nvidiaPlanHostUVMGPFIFOBytes nvidiaPlanHostPageBytes)
408
409def bobSemaphoreBytes : Nat =
410 (nvidiaPlanHostRoundUp
411 (naturalMultiply prSemaphoreStride bobSubmissionCount)
412 nvidiaPlanHostPageBytes)
413
414def bobStagingBytes : Nat =
415 (nvidiaPlanHostRoundUp bobArenaBytes nvidiaPlanHostMappingUnit)
416
417def bobSystemBuffer =
418 (lambda unrestricted identity : Bytes .
419 (lambda unrestricted gpu : Nat .
420 (lambda unrestricted host : Nat .
421 (lambda unrestricted extent : Nat .
422 (constructor
423 NvidiaPlanHostBuffer
424 NvidiaPlanHostBufferValue
425 identity
426 gpu
427 host
428 extent
429 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory))))))
430
431def bobVideoBuffer =
432 (lambda unrestricted identity : Bytes .
433 (lambda unrestricted gpu : Nat .
434 (lambda unrestricted host : Nat .
435 (lambda unrestricted extent : Nat .
436 (constructor
437 NvidiaPlanHostBuffer
438 NvidiaPlanHostBufferValue
439 identity
440 gpu
441 host
442 extent
443 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory))))))
444
445-- The layout: the GPFIFO and its USERD page in one video buffer, the
446-- pushbuffer, semaphores, program and QMD tables in system memory at the
447-- plan's bases, the staging buffer holding the arena. No external range
448-- (extent 0): nothing lives in video memory but the GPFIFO.
449def bobHostLayout =
450 (lambda unrestricted expectedName : Bytes .
451 (lambda unrestricted qmdLength : Nat .
452 (lambda unrestricted pushLength : Nat .
453 (constructor
454 NvidiaPlanHostLayout
455 NvidiaPlanHostLayoutValue
456 (bobVideoBuffer b"gpfifo+userd" bobGPFIFOBase bobHostGPFIFO bobGPFIFOBufferBytes)
457 (bobSystemBuffer
458 b"pushbuffer"
459 bobPushbufferBase
460 bobHostPushbuffer
461 (nvidiaPlanHostRoundUp pushLength nvidiaPlanHostMappingUnit))
462 (bobSystemBuffer b"semaphores" bobSemaphoreBase bobHostSemaphores bobSemaphoreBytes)
463 (bobSystemBuffer
464 b"program"
465 bobProgramBase
466 bobHostProgram
467 (nvidiaPlanHostRoundUp bobProgramBytes nvidiaPlanHostMappingUnit))
468 (bobSystemBuffer
469 b"qmd"
470 bobQMDBase
471 bobHostQMD
472 (nvidiaPlanHostRoundUp qmdLength nvidiaPlanHostMappingUnit))
473 (bobSystemBuffer
474 b"userd-alias"
475 (naturalAdd bobGPFIFOBase nvidiaPlanHostUVMGPFIFOBytes)
476 (naturalAdd bobHostGPFIFO nvidiaPlanHostUVMGPFIFOBytes)
477 nvidiaPlanHostPageBytes)
478 (constructor
479 NvidiaPlanHostBuffers
480 NvidiaPlanHostBuffersNext
481 (bobSystemBuffer b"arena" bobParametersAddress bobHostStaging bobStagingBytes)
482 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd))
483 nvidiaPlanHostAmpere580
484 (constructor NvidiaPlanHostLifecycle NvidiaPlanHostUVM 0 0)
485 expectedName
486 0))))
487
488def bobRecipeFills =
489 (lambda unrestricted qmdExpanded : Nat .
490 (lambda unrestricted pushExpanded : Nat .
491 (lambda unrestricted gpfifoExpanded : Nat .
492 (constructor
493 NvidiaPlanHostRecipeFills
494 NvidiaPlanHostRecipeFillsNext
495 bobHostProgram
496 bobProgramBytes
497 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable)
498 (constructor
499 NvidiaPlanHostRecipeFills
500 NvidiaPlanHostRecipeFillsNext
501 bobHostQMD
502 qmdExpanded
503 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable)
504 (constructor
505 NvidiaPlanHostRecipeFills
506 NvidiaPlanHostRecipeFillsNext
507 bobHostPushbuffer
508 pushExpanded
509 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer)
510 (constructor
511 NvidiaPlanHostRecipeFills
512 NvidiaPlanHostRecipeFillsNext
513 bobHostGPFIFO
514 gpfifoExpanded
515 (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO)
516 (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsEnd))))))))
517
518-- ---- the schedule ----
519def bobStagingAt =
520 (lambda unrestricted address : Nat .
521 (naturalAdd bobHostStaging (naturalSaturatingSubtract address bobParametersAddress)))
522
523def bobTrainingSubmissions : Nat =
524 (naturalSaturatingSubtract bobSubmissionCount bobForwardLaunches)
525
526def bobInput : (family NvidiaPlanHostFile) =
527 (constructor NvidiaPlanHostFile NvidiaPlanHostInput)
528
529def bobCheckpointIn : (family NvidiaPlanHostFile) =
530 (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointIn)
531
532def bobCheckpointOut : (family NvidiaPlanHostFile) =
533 (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut)
534
535def bobPredictions : (family NvidiaPlanHostFile) =
536 (constructor NvidiaPlanHostFile NvidiaPlanHostPredictions)
537
538def bobResult : (family NvidiaPlanHostFile) =
539 (constructor NvidiaPlanHostFile NvidiaPlanHostResult)
540
541def bobStepsEnd : (family NvidiaPlanHostSteps) =
542 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)
543
544def bobWriteAt =
545 (lambda unrestricted file : (family NvidiaPlanHostFile) .
546 (lambda unrestricted address : Nat .
547 (lambda unrestricted extent : Nat .
548 (lambda unrestricted offset : Nat .
549 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
550 (constructor
551 NvidiaPlanHostSteps
552 NvidiaPlanHostStepWriteAt
553 file
554 (bobStagingAt address)
555 extent
556 offset
557 tail))))))
558
559-- the results after the forward launches and after the training: the loss
560-- block of that phase, the logit rows, the predictions
561def bobWriteResults =
562 (lambda unrestricted lossAddress : Nat .
563 (lambda unrestricted lossOffset : Nat .
564 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
565 (constructor
566 NvidiaPlanHostSteps
567 NvidiaPlanHostStepBoundary
568 prTelemetryLearningValue
569 (aosChoose
570 Bytes
571 (naturalEqual lossAddress bobInitialLossAddress)
572 b"Bob:loss-before-training"
573 b"Bob:loss-after-training")
574 (bobWriteAt
575 bobResult
576 lossAddress
577 bobLossBytes
578 lossOffset
579 (bobWriteAt
580 bobResult
581 bobLogitRowsAddress
582 bobLogitRowsBytes
583 bobResultLogitRowsOffset
584 (bobWriteAt bobPredictions bobPredictionsAddress bobPredictionsBytes 0 tail)))))))
585
586def bobSubmitEachStep =
587 (lambda unrestricted count : Nat .
588 (lambda unrestricted firstGPPut : Nat .
589 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
590 (constructor
591 NvidiaPlanHostSteps
592 NvidiaPlanHostStepRepeat
593 count
594 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit firstGPPut 1 bobStepsEnd)
595 tail))))
596
597def bobHostSteps : (family NvidiaPlanHostSteps) =
598 (constructor
599 NvidiaPlanHostSteps
600 NvidiaPlanHostStepRead
601 bobInput
602 (bobStagingAt bobInputAddress)
603 bobInputRecordBytes
604 0
605 0
606 0
607 (constructor
608 NvidiaPlanHostSteps
609 NvidiaPlanHostStepRead
610 bobCheckpointIn
611 bobHostStaging
612 bobCheckpointPayloadBytes
613 0
614 0
615 1
616 (constructor
617 NvidiaPlanHostSteps
618 NvidiaPlanHostStepBoundary
619 prTelemetryStateRestored
620 b"request-host:checkpoint-restored"
621 (bobSubmitEachStep
622 bobForwardLaunches
623 1
624 (bobWriteResults
625 bobInitialLossAddress
626 bobResultInitialLossOffset
627 (constructor
628 NvidiaPlanHostSteps
629 NvidiaPlanHostStepOperation
630 (bobSubmitEachStep
631 bobTrainingSubmissions
632 (naturalAdd bobForwardLaunches 1)
633 (bobWriteResults
634 bobTrainingLossAddress
635 bobResultTrainingLossOffset
636 (bobWriteAt
637 bobCheckpointOut
638 bobParametersAddress
639 bobCheckpointPayloadBytes
640 0
641 (constructor
642 NvidiaPlanHostSteps
643 NvidiaPlanHostStepClose
644 bobCheckpointOut
645 (constructor
646 NvidiaPlanHostSteps
647 NvidiaPlanHostStepDataSync
648 bobPredictions
649 (constructor
650 NvidiaPlanHostSteps
651 NvidiaPlanHostStepDataSync
652 bobResult
653 bobStepsEnd))))))))))))
654
655-- ---- AdamW's step-dependent scalars ----
656def bobRealizedAddresses =
657 (lambda unrestricted realized : (family BobRealizedTables) .
658 (eliminate
659 BobRealizedTables
660 (lambda unrestricted current : (family BobRealizedTables) . Bytes)
661 realized
662 (branch BobRealizedTablesValue addresses words . addresses)))
663
664-- Bob's learner computes them in binary32 (Bob.Learner.bobAdamStepScalars);
665-- the host continues the step count from the checkpoint's header.
666def bobHostAdamW : (family NvidiaPlanHostAdamW) =
667 (constructor
668 NvidiaPlanHostAdamW
669 NvidiaPlanHostAdamWValue
670 (constructor NvidiaPlanHostArithmetic NvidiaPlanHostBinary32)
671 (constructor
672 NvidiaPlanHostConstant
673 NvidiaPlanHostBinary32Bits
674 (nvidiaPlanHostBinary32Of bobLearningRate))
675 (constructor
676 NvidiaPlanHostConstant
677 NvidiaPlanHostBinary32Bits
678 (nvidiaPlanHostBinary32Of bobBeta1))
679 (constructor
680 NvidiaPlanHostConstant
681 NvidiaPlanHostBinary32Bits
682 (nvidiaPlanHostBinary32Of bobBeta2))
683 (constructor
684 NvidiaPlanHostConstant
685 NvidiaPlanHostBinary32Bits
686 (nvidiaPlanHostBinary32Of bobEpsilon)))
687
688-- where the host writes: the step-size word of the parameter block (the
689-- epsilon beside it) of update k's AdamW launch
690def bobAdamWWordOffset : Nat =
691 (adamWF32CorrectedStepSizeOffsetOf adamWF32ABI)
692
693def bobAdamWLaunches =
694 (lambda unrestricted k : Nat .
695 (constructor StdList StdListCons Nat (bobAdamWLaunch k) (constructor StdList StdListEmpty Nat)))
696
697-- the word the plan bakes there for update k: step k + 1's step size and
698-- epsilon (Bob.Learner.bobAdamStepScalars, its seventh and eighth scalars)
699def bobAdamWBaked =
700 (lambda unrestricted k : Nat .
701 (nvidiaPlanHostLittleNatural
702 8
703 (dataBytesDropValidated (naturalMultiply 4 6) (bobAdamStepScalars (succ k)))))
704
705def bobHostLearner =
706 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
707 (lambda unrestricted addresses : Bytes .
708 (nvidiaPlanHostAdamWCommands
709 bobHostAdamW
710 bobUpdatesPerInvocation
711 (nvidiaPlanHostAdamWHostSites
712 layout
713 addresses
714 bobAdamWWordOffset
715 bobUpdatesPerInvocation
716 bobAdamWLaunches))))
717
718def bobHostLearnerAdmitted =
719 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
720 (lambda unrestricted realized : (family BobRealizedTables) .
721 (eliminate
722 BobRealizedTables
723 (lambda unrestricted current : (family BobRealizedTables) . Nat)
724 realized
725 (branch
726 BobRealizedTablesValue
727 addresses
728 words
729 .
730 (naturalAnd
731 (naturalEqual
732 (adamWF32ScaledEpsilonOffsetOf adamWF32ABI)
733 (naturalAdd bobAdamWWordOffset 4))
734 (nvidiaPlanHostAdamWSitesAdmitted
735 layout
736 addresses
737 words
738 bobAdamWWordOffset
739 bobUpdatesPerInvocation
740 bobAdamWLaunches
741 bobAdamWBaked))))))
742
743-- ---- contracts the pairing decides ----
744def bobHostSubmitsPlan : Nat =
745 (naturalEqual (nvidiaPlanHostStepSubmissions bobHostSteps) bobSubmissionCount)
746
747def bobHostMovesCheckpoint : Nat =
748 (naturalAnd
749 (nvidiaPlanHostFileReadsTile bobCheckpointIn bobCheckpointPayloadBytes bobHostSteps)
750 (naturalEqual
751 (nvidiaPlanHostStepBytesWritten bobCheckpointOut bobHostSteps)
752 bobCheckpointPayloadBytes))
753
754def bobHostCertified =
755 (lambda unrestricted qmdLength : Nat .
756 (lambda unrestricted pushLength : Nat .
757 (lambda unrestricted gpfifoLength : Nat .
758 (naturalAnd
759 bobHostSubmitsPlan
760 (naturalAnd
761 bobHostMovesCheckpoint
762 (nvidiaPlanHostRequestAdmitted
763 (bobHostLayout b"" qmdLength pushLength)
764 bobSubmissionCount
765 (bobRecipeFills qmdLength pushLength gpfifoLength)
766 bobHostSteps))))))
767
768-- the host's side (its schedule, and the AdamW sites the realization
769-- placed), then (only when it holds) the device's
770-- (Bob.Build.PhysicalComponents.bobDeviceHazard)
771def bobHostAdmitted =
772 (lambda unrestricted qmdLength : Nat .
773 (lambda unrestricted pushLength : Nat .
774 (lambda unrestricted gpfifoLength : Nat .
775 (lambda unrestricted realized : (family BobRealizedTables) .
776 (nat-eliminate
777 (lambda unrestricted host : Nat . Nat)
778 0
779 (lambda unrestricted p : Nat .
780 (lambda unrestricted ignored : Nat . (naturalIsZero (bobDeviceHazardOf p))))
781 (naturalAnd
782 (bobHostLearnerAdmitted (bobHostLayout b"" qmdLength pushLength) realized)
783 (bobHostCertified qmdLength pushLength gpfifoLength)))))))
784
785-- ---- the host ELF ----
786-- `productIdentity` is the pairing's padded card name: the host payload's
787-- identity in the envelope and the name the card must report.
788-- `hostWriter` makes the host program an executable for the pairing's host:
789-- Runtime.NativePhysicalNativeELF's direct writer for x86-64, Platform.
790-- AArch64.HostLowering's for the DGX Spark.
791def bobNativeCaptureBoundary =
792 (lambda unrestricted phase : Nat .
793 (lambda unrestricted name : Bytes .
794 (lambda unrestricted after : (family NativeObservedSteps) .
795 (aosChoose
796 (family NativeObservedSteps)
797 (naturalAnd
798 (naturalEqual phase prTelemetryLearningValue)
799 (bytes-equal name b"Bob:loss-before-training"))
800 (nvidiaRequestCaptureMappedF32
801 bobNativeRowTag0
802 (bobStagingAt bobInitialLossAddress)
803 (phLoad prGPPut)
804 after)
805 (aosChoose
806 (family NativeObservedSteps)
807 (naturalAnd
808 (naturalEqual phase prTelemetryLearningValue)
809 (bytes-equal name b"Bob:loss-after-training"))
810 (nvidiaRequestCaptureMappedF32
811 bobNativeRowTag1
812 (bobStagingAt bobTrainingLossAddress)
813 (phLoad prGPPut)
814 after)
815 (nvidiaRequestCaptureBoundaryWithCheckpoint phase name after))))))
816
817def bobNativeHostELFWithIdentitySource =
818 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
819 (lambda unrestricted hostWriter : (pi unrestricted program : (family NativePhysicalProgram) . Bytes) .
820 (lambda unrestricted productIdentity : Bytes .
821 (lambda unrestricted programIdentity : Bytes .
822 (lambda unrestricted qmdIdentity : Bytes .
823 (lambda unrestricted pushIdentity : Bytes .
824 (lambda unrestricted gpfifoIdentity : Bytes .
825 (lambda unrestricted programLength : Nat .
826 (lambda unrestricted qmdLength : Nat .
827 (lambda unrestricted pushLength : Nat .
828 (lambda unrestricted gpfifoLength : Nat .
829 (lambda unrestricted qmdExpanded : Nat .
830 (lambda unrestricted pushExpanded : Nat .
831 (lambda unrestricted gpfifoExpanded : Nat .
832 (lambda unrestricted realized : (family BobRealizedTables) .
833 (nat-eliminate
834 (lambda unrestricted admitted : Nat . Bytes)
835 b""
836 (lambda unrestricted predecessor : Nat .
837 (lambda unrestricted induction : Bytes .
838 (hostWriter
839 (nvidiaPlanHostManagedRequestProgramWithBoundary
840 bobNativeCaptureBoundary
841 source
842 bobNativeRequestCapturePlan
843 (bobHostLayout productIdentity qmdExpanded pushExpanded)
844 productIdentity
845 programIdentity
846 qmdIdentity
847 pushIdentity
848 gpfifoIdentity
849 programLength
850 qmdLength
851 pushLength
852 gpfifoLength
853 bobSubmissionCount
854 (constructor
855 NvidiaPlanHostInputContract
856 NvidiaPlanHostInputExact
857 bobInputRecordBytes)
858 bobCheckpointContract
859 (bobRecipeFills qmdExpanded pushExpanded gpfifoExpanded)
860 (bobHostLearner
861 (bobHostLayout productIdentity qmdExpanded pushExpanded)
862 (bobRealizedAddresses realized))
863 bobHostSteps))))
864 (bobHostAdmitted qmdExpanded pushExpanded gpfifoExpanded realized)))))))))))))))))
865
866-- Existing pairings retain fresh identities unless the artifact explicitly
867-- declares an assigned input. No environment-dependent runtime fallback.
868def bobNativeHostELF =
869 (bobNativeHostELFWithIdentitySource
870 (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity))
871
872-- ---- what the artifact demands of a card (Platform.Linux.Nvidia.Compatibility) ----
873-- the instruction set its QMDs are built for, its kernels' resources, the
874-- video memory it reserves, and its host's driver branch, compute class and
875-- unified memory; a pairing admits a card whose profile supplies them all
876def bobCompatDemands =
877 (lambda unrestricted architecture : (family ModelWord32) .
878 (nvidiaPlanDemands
879 (nvidiaInstructionSetOf (modelWord32ToNatural architecture))
880 bobRegions
881 bobMinimumVideoBytes
882 (nvidiaHostDemands (bobHostLayout b"" 0 0) nvidiaNoDemands)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.