1module Hardware.Nvidia.SM86.Command.WholeProgramPlan
2
3import Accelerator.SM86.Instruction
4import Accelerator.SM86.InstructionEncoding
5import Accelerator.SM86.Program
6import Hardware.Nvidia.SM86.Command.QMD
7import Std.Natural
8import Std.Foundation
9import Std.List
10import Data.Bytes
11import Model.Config
12import Model.Parameter
13import Model.Word64
14
15-- A program's machine code on a target that does not run its SM86 words
16-- (sm_121's: Accelerator.SM121.Lowering), or why it has none.
17family NvidiaDeviceRealization : Type 0
18constructor NvidiaDeviceRealized
19field unrestricted nvidiaDeviceRealizedMaterial : Bytes
20constructor NvidiaDeviceRealizationRefused
21field unrestricted nvidiaDeviceRealizationRefusal : Bytes
22end-family
23
24-- Target-owned, typed inputs to late NVIDIA component realization. These
25-- values remain ordinary Alpha data until whole-program erasure has selected a
26-- concrete target. `compiler-native-encode` is the backend boundary: it
27-- lowers this public representation without making a model own wire layouts.
28family NvidiaDeviceRegion : Type 0
29constructor NvidiaDeviceRegionValue
30field unrestricted nvidiaDeviceRegionIdentity : Bytes
31field unrestricted nvidiaDeviceRegionMaterial : Bytes
32field unrestricted nvidiaDeviceRegionRegisters : Nat
33field unrestricted nvidiaDeviceRegionBlockX : Nat
34field unrestricted nvidiaDeviceRegionSharedBytes : Nat
35-- SM121 needs an explicit barrier allocation. The older constructor cannot
36-- be silently reinterpreted as Blackwell: its resource contract lacks this
37-- field and its machine image belongs to another instruction profile.
38constructor NvidiaDeviceRegionSM121
39field unrestricted nvidiaSM121RegionIdentity : Bytes
40field unrestricted nvidiaSM121RegionMaterial : Bytes
41field unrestricted nvidiaSM121RegionRegisters : Nat
42field unrestricted nvidiaSM121RegionBlockX : Nat
43field unrestricted nvidiaSM121RegionSharedBytes : Nat
44field unrestricted nvidiaSM121RegionBarrierCount : Nat
45-- A region given as its typed SM86 program: its canonical placement is the
46-- program's SM86 encoding, and the backend places the machine code of the
47-- plan's target: the SM86 words, or the sm_121 realization (read only for an
48-- sm_121 plan).
49constructor NvidiaDeviceProgramRegion
50field unrestricted nvidiaDeviceProgramRegionIdentity : Bytes
51field unrestricted nvidiaDeviceProgramRegionProgram : (family SM86Program)
52field unrestricted nvidiaDeviceProgramRegionRegisters : Nat
53field unrestricted nvidiaDeviceProgramRegionBlockX : Nat
54field unrestricted nvidiaDeviceProgramRegionSharedBytes : Nat
55field unrestricted nvidiaDeviceProgramRegionSM121 : (family NvidiaDeviceRealization)
56end-family
57
58family NvidiaDeviceRegions : Type 0
59constructor NvidiaDeviceRegionsEnd
60constructor NvidiaDeviceRegionsNext
61field unrestricted nvidiaDeviceRegionsHead : (family NvidiaDeviceRegion)
62recursive unrestricted nvidiaDeviceRegionsTail
63end-family
64
65-- Kernel parameters remain typed sparse words until late realization. The
66-- backend supplies zero-filled storage, checks every word offset against the
67-- launch's declared constant extent, and chooses the final program or spill
68-- address only after device-region erasure and compaction.
69family NvidiaParameterPatch : Type 0
70constructor NvidiaParameterPatchValue
71field unrestricted nvidiaParameterPatchWordOffset : Nat
72field unrestricted nvidiaParameterPatchWordValue : (family ModelWord64)
73end-family
74
75family NvidiaParameterPatches : Type 0
76constructor NvidiaParameterPatchesEnd
77constructor NvidiaParameterPatchesNext
78field unrestricted nvidiaParameterPatchesHead : (family NvidiaParameterPatch)
79recursive unrestricted nvidiaParameterPatchesTail
80end-family
81
82family NvidiaParameterBlock : Type 0
83constructor NvidiaParameterBlockValue
84field unrestricted nvidiaParameterBlockPatches : (family NvidiaParameterPatches)
85end-family
86
87-- Repeat adjustments name a block ordinal within the expanded repeated body,
88-- or every block when one training scalar is shared by a phase. Affine and
89-- quotient/remainder adjustments are deltas; table frames are exact values.
90family NvidiaParameterAdjustmentScope : Type 0
91constructor NvidiaParameterAdjustmentAllBlocks
92constructor NvidiaParameterAdjustmentBlock
93field unrestricted nvidiaParameterAdjustmentBlockOrdinal : Nat
94end-family
95
96family NvidiaParameterAdjustment : Type 0
97constructor NvidiaParameterAdjustmentValue
98field unrestricted nvidiaParameterAdjustmentScope : (family NvidiaParameterAdjustmentScope)
99field unrestricted nvidiaParameterAdjustmentWordOffset : Nat
100field unrestricted nvidiaParameterAdjustmentWordValue : (family ModelWord64)
101end-family
102
103family NvidiaParameterAdjustments : Type 0
104constructor NvidiaParameterAdjustmentsEnd
105constructor NvidiaParameterAdjustmentsNext
106field unrestricted nvidiaParameterAdjustmentsHead : (family NvidiaParameterAdjustment)
107recursive unrestricted nvidiaParameterAdjustmentsTail
108end-family
109
110family NvidiaParameterAdjustmentFrames : Type 0
111constructor NvidiaParameterAdjustmentFramesEnd
112constructor NvidiaParameterAdjustmentFramesNext
113field unrestricted nvidiaParameterAdjustmentFrame : (family NvidiaParameterAdjustments)
114recursive unrestricted nvidiaParameterAdjustmentFramesTail
115end-family
116
117family NvidiaParameterIteration : Type 0
118constructor NvidiaParameterIterationUnchanged
119constructor NvidiaParameterIterationAffine
120field unrestricted nvidiaParameterIterationAffineDeltas : (family NvidiaParameterAdjustments)
121constructor NvidiaParameterIterationQuotientRemainder
122field unrestricted nvidiaParameterIterationDivisor : Nat
123field unrestricted nvidiaParameterIterationRemainderDeltas : (family NvidiaParameterAdjustments)
124field unrestricted nvidiaParameterIterationQuotientDeltas : (family NvidiaParameterAdjustments)
125constructor NvidiaParameterIterationTable
126field unrestricted nvidiaParameterIterationFrames : (family NvidiaParameterAdjustmentFrames)
127end-family
128
129-- A launch names a typed device region by its pre-compaction address and
130-- carries only semantic launch geometry and constant-buffer placement. Code
131-- extent, prefetch width, block X, register count and shared memory are
132-- deliberately absent: the backend derives those fields from the retained
133-- device region after whole-program erasure.
134family NvidiaLaunchKernel : Type 0
135constructor NvidiaLaunchKernelValue
136field unrestricted nvidiaLaunchProgramAddress : (family ModelWord64)
137field unrestricted nvidiaLaunchGridX : Nat
138field unrestricted nvidiaLaunchGridY : Nat
139field unrestricted nvidiaLaunchGridZ : Nat
140field unrestricted nvidiaLaunchBlockY : Nat
141field unrestricted nvidiaLaunchBlockZ : Nat
142field unrestricted nvidiaLaunchConstantBytes : Nat
143end-family
144
145family NvidiaLaunchTemplate : Type 0
146constructor NvidiaLaunchTemplateValue
147field unrestricted nvidiaLaunchSourceIdentity : Bytes
148field unrestricted nvidiaLaunchKernel : (family NvidiaLaunchKernel)
149field unrestricted nvidiaLaunchParameters : (family NvidiaParameterBlock)
150end-family
151
152-- Repeated training phases stay compact in source. Parameter iteration
153-- metadata transforms sparse words without duplicating parameter blocks,
154-- device images or descriptor bytes in the checked graph.
155family NvidiaLaunchSchedule : Type 0
156constructor NvidiaLaunchScheduleEmpty
157constructor NvidiaLaunchScheduleOne
158field unrestricted nvidiaLaunchScheduleLaunch : (family NvidiaLaunchTemplate)
159constructor NvidiaLaunchScheduleAppend
160recursive unrestricted nvidiaLaunchScheduleLeft
161recursive unrestricted nvidiaLaunchScheduleRight
162constructor NvidiaLaunchScheduleRepeat
163field unrestricted nvidiaLaunchScheduleRepeatCount : Nat
164field unrestricted nvidiaLaunchScheduleParameterIteration : (family NvidiaParameterIteration)
165recursive unrestricted nvidiaLaunchScheduleRepeatedBody
166end-family
167
168-- Submission ranges refer to ordinals in the realized QMD table. Pushbuffer
169-- methods and GPFIFO entries are derived from these ranges after launch
170-- erasure; neither their addresses nor padding are frozen in model source.
171family NvidiaLaunchReferences : Type 0
172constructor NvidiaLaunchReferencesEmpty
173constructor NvidiaLaunchReferencesRange
174field unrestricted nvidiaLaunchReferenceFirst : Nat
175field unrestricted nvidiaLaunchReferenceCount : Nat
176constructor NvidiaLaunchReferencesAppend
177recursive unrestricted nvidiaLaunchReferencesLeft
178recursive unrestricted nvidiaLaunchReferencesRight
179end-family
180
181family NvidiaSubmissionBatch : Type 0
182constructor NvidiaSubmissionBatchValue
183field unrestricted nvidiaSubmissionSourceIdentity : Bytes
184field unrestricted nvidiaSubmissionSemaphoreOffset : Nat
185field unrestricted nvidiaSubmissionReferences : (family NvidiaLaunchReferences)
186end-family
187
188family NvidiaSubmissionSchedule : Type 0
189constructor NvidiaSubmissionScheduleEmpty
190constructor NvidiaSubmissionScheduleOne
191field unrestricted nvidiaSubmissionScheduleBatch : (family NvidiaSubmissionBatch)
192constructor NvidiaSubmissionScheduleAppend
193recursive unrestricted nvidiaSubmissionScheduleLeft
194recursive unrestricted nvidiaSubmissionScheduleRight
195constructor NvidiaSubmissionScheduleRepeat
196field unrestricted nvidiaSubmissionScheduleRepeatCount : Nat
197field unrestricted nvidiaSubmissionReferenceStride : Nat
198field unrestricted nvidiaSubmissionSemaphoreStride : Nat
199recursive unrestricted nvidiaSubmissionScheduleRepeatedBody
200-- The same submissions, each launch followed by a semaphore release that
201-- waits for it to finish and carries the device's timestamp, at `offset` +
202-- 16 x the launch's QMD ordinal from the plan's semaphore base (its payload
203-- the ordinal): the device time of every launch, for a profile. Waiting for
204-- each launch serializes launches the plan would otherwise let overlap, so a
205-- profile's step is not the production step's time.
206constructor NvidiaSubmissionScheduleProfiled
207field unrestricted nvidiaSubmissionProfileOffset : Nat
208recursive unrestricted nvidiaSubmissionProfiledBody
209end-family
210
211family NvidiaQMDRecipeBlocks : Type 0
212constructor NvidiaQMDRecipeBlocksEnd
213constructor NvidiaQMDRecipeBlocksNext
214field unrestricted nvidiaQMDRecipeBlockIdentity : Bytes
215field unrestricted nvidiaQMDRecipeBlockOutputBytes : (family ModelWord64)
216field unrestricted nvidiaQMDRecipeBlockRecordCount : Nat
217field unrestricted nvidiaQMDRecipeBlockZeroRecords : Nat
218field unrestricted nvidiaQMDRecipeBlockRecords : Bytes
219recursive unrestricted nvidiaQMDRecipeBlocksTail
220end-family
221
222family NvidiaPackbitsRecipeBlocks : Type 0
223constructor NvidiaPackbitsRecipeBlocksEnd
224constructor NvidiaPackbitsRecipeBlocksNext
225field unrestricted nvidiaPackbitsRecipeBlockIdentity : Bytes
226field unrestricted nvidiaPackbitsRecipeBlockOutputBytes : (family ModelWord64)
227field unrestricted nvidiaPackbitsRecipeBlockCommandCount : Nat
228field unrestricted nvidiaPackbitsRecipeBlockBytes : Bytes
229recursive unrestricted nvidiaPackbitsRecipeBlocksTail
230end-family
231
232family NvidiaPushRecipeBlocks : Type 0
233constructor NvidiaPushRecipeBlocksEnd
234constructor NvidiaPushRecipeBlocksNext
235field unrestricted nvidiaPushRecipeBlockPushIdentity : Bytes
236field unrestricted nvidiaPushRecipeBlockPushBytes : (family ModelWord64)
237field unrestricted nvidiaPushRecipeBlockGPFIFOIdentity : Bytes
238field unrestricted nvidiaPushRecipeBlockGPFIFOBytes : (family ModelWord64)
239field unrestricted nvidiaPushRecipeBlockBatchCount : Nat
240field unrestricted nvidiaPushRecipeBlockBatches : Bytes
241recursive unrestricted nvidiaPushRecipeBlocksTail
242end-family
243
244family NvidiaPhysicalComponentPlan : Type 0
245constructor NvidiaProgramComponentPlan
246field unrestricted nvidiaProgramImages : Bytes
247field unrestricted nvidiaProgramImageCursor : Nat
248field unrestricted nvidiaProgramImageCount : Nat
249field unrestricted nvidiaProgramExpectedImageCursor : Nat
250field unrestricted nvidiaProgramExpectedImageCount : Nat
251field unrestricted nvidiaProgramGapBytes : Nat
252field unrestricted nvidiaProgramRecipeCommands : Nat
253field unrestricted nvidiaProgramRecipe : Bytes
254field unrestricted nvidiaProgramRecipeDropBytes : Nat
255field unrestricted nvidiaProgramOutputBytes : Nat
256constructor NvidiaQMDComponentPlan
257field unrestricted nvidiaQMDArchitecture : (family ModelWord32)
258field unrestricted nvidiaQMDBlocks : (family NvidiaQMDRecipeBlocks)
259constructor NvidiaPackbitsComponentPlan
260field unrestricted nvidiaPackbitsPrefixZeroBytes : Nat
261field unrestricted nvidiaPackbitsBlocks : (family NvidiaPackbitsRecipeBlocks)
262constructor NvidiaPushComponentPlan
263field unrestricted nvidiaPushComputeClass : (family ModelWord32)
264field unrestricted nvidiaPushSPAVersion : (family ModelWord32)
265field unrestricted nvidiaPushBlocks : (family NvidiaPushRecipeBlocks)
266constructor NvidiaGPFIFOComponentPlan
267field unrestricted nvidiaGPFIFOComputeClass : (family ModelWord32)
268field unrestricted nvidiaGPFIFOSPAVersion : (family ModelWord32)
269field unrestricted nvidiaGPFIFOBlocks : (family NvidiaPushRecipeBlocks)
270end-family
271
272-- One connected late-realization plan. Program compaction and QMD rewriting
273-- consume this value together, so a descriptor cannot retain an address or a
274-- resource count from an erased or superseded device region. The historical
275-- recipe parameter offset and component capacity are compatibility bounds for
276-- the current host protocol, not output-layout requirements: retained images
277-- are repacked and their QMD fields are derived again before the component is
278-- padded to the admitted arena capacity.
279family NvidiaWholeProgramComponent : Type 0
280constructor NvidiaWholeProgramProgram
281constructor NvidiaWholeProgramQMD
282constructor NvidiaWholeProgramPushbuffer
283constructor NvidiaWholeProgramGPFIFO
284-- The same four tables as launch-table recipes: the compact form the host
285-- expands into the mapped arena at startup with the shared
286-- Runtime.NativeLaunchRecipeRoutine. The compiler derives each recipe from
287-- the schedule's repeat structure and publishes it only after it has expanded
288-- it back to the exact table bytes.
289constructor NvidiaWholeProgramProgramRecipe
290constructor NvidiaWholeProgramQMDRecipe
291constructor NvidiaWholeProgramPushbufferRecipe
292constructor NvidiaWholeProgramGPFIFORecipe
293-- The device address of each launch's parameter block, in launch order (a
294-- little-endian u64 each), as the realization placed it: in the program
295-- region after the retained code, or past the QMD table. A host that
296-- supplies a parameter word at run time writes it there.
297constructor NvidiaWholeProgramParameterAddresses
298-- The 8-byte word at a byte offset of each launch's parameter block, in
299-- launch order, as realized (0 past the block's extent): what a host that
300-- supplies a word at run time checks its sites against.
301constructor NvidiaWholeProgramParameterWords
302field unrestricted nvidiaWholeProgramParameterWordOffset : Nat
303-- The launch manifest, one text line per launch in QMD order: the ordinal,
304-- the launch's source identity and its device region's identity, separated
305-- by tabs. A per-launch profile (NvidiaSubmissionScheduleProfiled) records
306-- one stamp per QMD ordinal; the manifest names what each ordinal ran.
307constructor NvidiaWholeProgramLaunchIdentities
308end-family
309
310family NvidiaWholeProgramPlan : Type 0
311constructor NvidiaWholeProgramPlanValue
312field unrestricted nvidiaWholeProgramComponent : (family NvidiaWholeProgramComponent)
313field unrestricted nvidiaWholeProgramArchitecture : (family ModelWord32)
314field unrestricted nvidiaWholeProgramComputeClass : (family ModelWord32)
315field unrestricted nvidiaWholeProgramSPAVersion : (family ModelWord32)
316field unrestricted nvidiaWholeProgramProgramBase : (family ModelWord64)
317field unrestricted nvidiaWholeProgramQMDBase : (family ModelWord64)
318field unrestricted nvidiaWholeProgramPushbufferBase : (family ModelWord64)
319field unrestricted nvidiaWholeProgramSemaphoreBase : (family ModelWord64)
320field unrestricted nvidiaWholeProgramRegionAlignment : Nat
321field unrestricted nvidiaWholeProgramProgramCapacity : Nat
322field unrestricted nvidiaWholeProgramRegions : (family NvidiaDeviceRegions)
323field unrestricted nvidiaWholeProgramLaunchSchedule : (family NvidiaLaunchSchedule)
324field unrestricted nvidiaWholeProgramExpectedLaunchCount : Nat
325field unrestricted nvidiaWholeProgramQMDTableBytes : Nat
326field unrestricted nvidiaWholeProgramSubmissions : (family NvidiaSubmissionSchedule)
327field unrestricted nvidiaWholeProgramExpectedSubmissionCount : Nat
328field unrestricted nvidiaWholeProgramExpectedReferenceCount : Nat
329end-family
330
331def nvidiaLaunchFirstOrdinal : Nat = 0
332def nvidiaSubmissionFirstSemaphoreOffset : Nat = 0
333
334def nvidiaLaunchReferencesCount =
335 (lambda unrestricted references : (family NvidiaLaunchReferences) .
336 (eliminate NvidiaLaunchReferences
337 (lambda unrestricted current : (family NvidiaLaunchReferences) . Nat)
338 references
339 (branch NvidiaLaunchReferencesEmpty . 0)
340 (branch NvidiaLaunchReferencesRange first count . count)
341 (branch NvidiaLaunchReferencesAppend left right leftCount rightCount .
342 (naturalAdd leftCount rightCount))))
343def nvidiaSubmissionScheduleCount =
344 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
345 (eliminate NvidiaSubmissionSchedule
346 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
347 schedule
348 (branch NvidiaSubmissionScheduleEmpty . 0)
349 (branch NvidiaSubmissionScheduleOne batch . 1)
350 (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount .
351 (naturalAdd leftCount rightCount))
352 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount .
353 (naturalMultiply count bodyCount))
354 (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount)))
355def nvidiaSubmissionScheduleReferenceCount =
356 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
357 (eliminate NvidiaSubmissionSchedule
358 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
359 schedule
360 (branch NvidiaSubmissionScheduleEmpty . 0)
361 (branch NvidiaSubmissionScheduleOne batch .
362 (eliminate NvidiaSubmissionBatch
363 (lambda unrestricted current : (family NvidiaSubmissionBatch) . Nat)
364 batch
365 (branch NvidiaSubmissionBatchValue identity semaphore references .
366 (nvidiaLaunchReferencesCount references))))
367 (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount .
368 (naturalAdd leftCount rightCount))
369 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount .
370 (naturalMultiply count bodyCount))
371 (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount)))
372
373-- A launch can declare ordered, typed patches without nesting one constructor
374-- per ABI argument. Validation of offsets and extent still belongs to the
375-- late parameter-block realization, after image pruning and placement.
376def nvidiaParameterPatchesFromList =
377 (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) .
378 (eliminate StdList
379 (lambda unrestricted current : (family StdList (family NvidiaParameterPatch)) .
380 (family NvidiaParameterPatches))
381 patches
382 (branch StdListEmpty .
383 (constructor NvidiaParameterPatches NvidiaParameterPatchesEnd))
384 (branch StdListCons head tail induction .
385 (constructor NvidiaParameterPatches NvidiaParameterPatchesNext
386 head induction))))
387def nvidiaParameterBlockFromList =
388 (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) .
389 (constructor NvidiaParameterBlock NvidiaParameterBlockValue
390 (nvidiaParameterPatchesFromList patches)))
391
392-- A layer may reuse the same typed image and launch geometry while its
393-- parameter pointers change. Keeping identity and kernel together prevents
394-- callers from restating hardware launch facts for each layer.
395def nvidiaLaunchWithParameters =
396 (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
397 (lambda unrestricted parameters : (family NvidiaParameterBlock) .
398 (eliminate NvidiaLaunchTemplate
399 (lambda unrestricted current : (family NvidiaLaunchTemplate) .
400 (family NvidiaLaunchTemplate)) launch
401 (branch NvidiaLaunchTemplateValue identity kernel previous .
402 (constructor NvidiaLaunchTemplate NvidiaLaunchTemplateValue
403 identity kernel parameters)))))
404def nvidiaLaunchSequence =
405 (lambda unrestricted launches : (family StdList (family NvidiaLaunchTemplate)) .
406 (stdListFold (family NvidiaLaunchTemplate) (family NvidiaLaunchSchedule)
407 (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
408 (lambda unrestricted tail : (family NvidiaLaunchSchedule) .
409 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleAppend
410 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleOne launch) tail)))
411 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleEmpty) launches))
412
413-- CB0 uses 64-bit pointer slots after the target QMD parameter header.
414-- Systems supply addresses from their arena layout, not literal word slots.
415def nvidiaKernelBlockXWord : Nat =
416 (naturalDivideUnchecked qmdBlockDimensionXOffset 8)
417def nvidiaKernelPointerSlotBytes : Nat = 8
418def nvidiaKernelPointerByteOffset =
419 (lambda unrestricted argument : Nat .
420 (naturalAdd qmdKernelParameterBase
421 (naturalMultiply nvidiaKernelPointerSlotBytes argument)))
422def nvidiaKernelPointerWord =
423 (lambda unrestricted argument : Nat .
424 (naturalDivideUnchecked (nvidiaKernelPointerByteOffset argument)
425 nvidiaKernelPointerSlotBytes))
426def nvidiaKernelPointerPatch =
427 (lambda unrestricted argument : Nat . (lambda unrestricted address : Nat .
428 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
429 (nvidiaKernelPointerWord argument)
430 (modelWord64FromNaturalTruncated address))))
431def nvidiaKernelU32WordPatch =
432 (lambda unrestricted slot : Nat . (lambda unrestricted word : Nat .
433 (lambda erased admitted :
434 (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) .
435 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
436 slot (modelWord64FromNaturalTruncated word)))))
437-- Two neighboring 32-bit CB0 scalars share one 64-bit sparse patch. Packing
438-- them here prevents a later patch from overwriting the first scalar.
439def nvidiaKernelU32PairPatch =
440 (lambda unrestricted argument : Nat .
441 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
442 (lambda erased lowAdmitted :
443 (equal Nat (naturalLess low (naturalPowerOfTwo 32)) 1) .
444 (lambda erased highAdmitted :
445 (equal Nat (naturalLess high (naturalPowerOfTwo 32)) 1) .
446 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
447 (nvidiaKernelPointerWord argument)
448 (modelWord64FromNaturalTruncated
449 (naturalAdd low (naturalMultiply high (naturalPowerOfTwo 32))))))))))
450-- A whole-table certificate admits dynamic indices whose selected values
451-- cannot be reduced while checking a launch-construction lambda. An index
452-- beyond the list yields zero; the schedule owner separately proves length.
453def nvidiaKernelU32TableOverflowCount =
454 (lambda unrestricted table : (family StdList Nat) .
455 (stdListFold Nat Nat
456 (lambda unrestricted word : Nat . (lambda unrestricted count : Nat .
457 (naturalAdd count
458 (naturalSelect (naturalLess word (naturalPowerOfTwo 32)) 0 1))))
459 0 table))
460def nvidiaKernelU32TableWordAt =
461 (lambda unrestricted table : (family StdList Nat) .
462 (lambda unrestricted index : Nat .
463 (stdOptionValueOr Nat 0 (stdListIndex Nat table index))))
464def nvidiaKernelU32PairPatchFromCertifiedTable =
465 (lambda unrestricted argument : Nat .
466 (lambda unrestricted table : (family StdList Nat) .
467 (lambda unrestricted index : Nat .
468 (lambda erased admitted :
469 (equal Nat (nvidiaKernelU32TableOverflowCount table) 0) .
470 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
471 (nvidiaKernelPointerWord argument)
472 (modelWord64FromNaturalTruncated
473 (naturalAdd
474 (nvidiaKernelU32TableWordAt table index)
475 (naturalMultiply
476 (nvidiaKernelU32TableWordAt table (succ index))
477 (naturalPowerOfTwo 32)))))))))
478def nvidiaKernelF32ScalarPatch =
479 (lambda unrestricted argument : Nat . (lambda unrestricted word : Nat .
480 (lambda erased admitted :
481 (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) .
482 (nvidiaKernelU32WordPatch
483 (nvidiaKernelPointerWord argument) word admitted))))
484
485-- Compose independently owned device closures before whole-program pruning.
486-- This preserves order; placement and duplicate-identity admission remain
487-- the whole-program planner's responsibility.
488def nvidiaAppendDeviceRegions =
489 (lambda unrestricted left : (family NvidiaDeviceRegions) .
490 (lambda unrestricted right : (family NvidiaDeviceRegions) .
491 (eliminate NvidiaDeviceRegions
492 (lambda unrestricted current : (family NvidiaDeviceRegions) . (family NvidiaDeviceRegions)) left
493 (branch NvidiaDeviceRegionsEnd . right)
494 (branch NvidiaDeviceRegionsNext head tail induction .
495 (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext head induction)))))
496
497-- how many launches a schedule expands to
498-- Extents of the v1 submission protocol used by the backend: initialization
499-- has four two-word methods, three three-word methods, and 64 two-word CWD
500-- counter methods. Each of the two semaphore releases is six words; a launch
501-- is three two-word methods. Keep sizing separate from byte encoding so a
502-- placement proof need not normalize a machine image. Artifact gates compare
503-- this extent with the backend's actual output before accepting the image.
504def nvidiaCodeRegionAlignment : Nat = 256
505def nvidiaCodeRegionExtent = (lambda unrestricted bytes : Nat .
506 (naturalMultiply nvidiaCodeRegionAlignment
507 (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1)) nvidiaCodeRegionAlignment)))
508-- SM86 placement uses the same 256-byte alignment and 16-byte instruction
509-- extent as nativePlaceNvidiaRegions. A target-specific lookup is required:
510-- SM121 lowering can change a typed program's byte extent.
511def nvidiaSM86RegionIdentity =
512 (lambda unrestricted region : (family NvidiaDeviceRegion) .
513 (eliminate NvidiaDeviceRegion
514 (lambda unrestricted current : (family NvidiaDeviceRegion) . Bytes) region
515 (branch NvidiaDeviceRegionValue identity material registers block shared . identity)
516 (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . identity)
517 (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget . identity)))
518def nvidiaSM86RegionExtent =
519 (lambda unrestricted region : (family NvidiaDeviceRegion) .
520 (eliminate NvidiaDeviceRegion
521 (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
522 (branch NvidiaDeviceRegionValue identity material registers block shared . (bytes-length material))
523 (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . 0)
524 (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget .
525 (naturalMultiply sm86InstructionBytes (sm86ProgramCount program)))))
526def nvidiaSM86RegionsAdmitted =
527 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
528 (eliminate NvidiaDeviceRegions
529 (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
530 (branch NvidiaDeviceRegionsEnd . 1)
531 (branch NvidiaDeviceRegionsNext head tail induction .
532 (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head)) induction))))
533-- The end of the canonical region placement, before reachability pruning.
534-- A program arena sized from this upper bound remains valid when a launch
535-- disappears or code is compacted; each region starts at the same alignment
536-- nativePlaceNvidiaRegions uses for SM86.
537def nvidiaSM86RegionsPlacedEnd =
538 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
539 (app
540 (eliminate NvidiaDeviceRegions
541 (lambda unrestricted current : (family NvidiaDeviceRegions) .
542 (pi unrestricted cursor : Nat . Nat)) regions
543 (branch NvidiaDeviceRegionsEnd .
544 (lambda unrestricted cursor : Nat . cursor))
545 (branch NvidiaDeviceRegionsNext head tail induction .
546 (lambda unrestricted cursor : Nat .
547 (induction (naturalAdd (nvidiaCodeRegionExtent cursor)
548 (nvidiaSM86RegionExtent head))))))
549 0))
550def nvidiaSM86RegionPrefixAdmitted =
551 (lambda unrestricted identity : Bytes .
552 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
553 (eliminate NvidiaDeviceRegions
554 (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
555 (branch NvidiaDeviceRegionsEnd . 0)
556 (branch NvidiaDeviceRegionsNext head tail induction .
557 (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head))
558 (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity)
559 1 induction))))))
560def nvidiaSM86RegionOffsetFrom =
561 (lambda unrestricted identity : Bytes .
562 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
563 (eliminate NvidiaDeviceRegions
564 (lambda unrestricted current : (family NvidiaDeviceRegions) . (pi unrestricted cursor : Nat . Nat)) regions
565 (branch NvidiaDeviceRegionsEnd . (lambda unrestricted cursor : Nat . 0))
566 (branch NvidiaDeviceRegionsNext head tail induction .
567 (lambda unrestricted cursor : Nat .
568 (let unrestricted placed = (nvidiaCodeRegionExtent cursor) in
569 (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity)
570 placed
571 (induction (naturalAdd placed (nvidiaSM86RegionExtent head))))))))))
572def nvidiaSM86RegionAddressAdmitted =
573 (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes .
574 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
575 (naturalAnd (naturalNonzero base)
576 (naturalAnd (naturalIsZero (naturalModuloUnchecked base nvidiaCodeRegionAlignment))
577 (nvidiaSM86RegionPrefixAdmitted identity regions))))))
578def nvidiaSM86RegionAddress =
579 (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes .
580 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
581 (lambda erased admitted :
582 (equal Nat (nvidiaSM86RegionAddressAdmitted base identity regions) 1) .
583 (naturalAdd base (nvidiaSM86RegionOffsetFrom identity regions 0))))))
584-- CB0 extents are rounded to QMD's sixteen-byte size unit, independently
585-- of the stronger alignment imposed on the parameter block's device VA.
586def nvidiaKernelConstantExtentUnit : Nat = 16
587def nvidiaKernelConstantExtent = (lambda unrestricted argumentEnd : Nat .
588 (naturalMultiply nvidiaKernelConstantExtentUnit
589 (naturalDivideUnchecked (naturalAdd argumentEnd (naturalSaturatingSubtract nvidiaKernelConstantExtentUnit 1))
590 nvidiaKernelConstantExtentUnit)))
591def nvidiaSM121ConstantExtentUnit : Nat = nvidiaKernelConstantExtentUnit
592def nvidiaSM121ConstantExtent = nvidiaKernelConstantExtent
593def nvidiaSM121QMDRecordBytes : Nat = (naturalMultiply 96 4)
594def nvidiaSM121QMDSlotBytes : Nat =
595 (naturalMultiply nvidiaCodeRegionAlignment
596 (naturalDivideUnchecked (naturalAdd nvidiaSM121QMDRecordBytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1))
597 nvidiaCodeRegionAlignment))
598def nvidiaSubmissionWordBytes : Nat = 4
599def nvidiaSubmissionBatchBytes = (lambda unrestricted launches : Nat .
600 (naturalMultiply nvidiaSubmissionWordBytes
601 (naturalAdd (naturalAdd (naturalMultiply 2 (naturalAdd 4 64)) (naturalMultiply 3 3))
602 (naturalAdd (naturalMultiply 2 6) (naturalMultiply launches (naturalMultiply 3 2))))))
603-- A Blackwell batch is encoded as an Ampere one (the backend's
604-- nativeEncodeNvidiaSubmissionPieces, one target abstraction since the
605-- 2026-09-26 merge): the compute initialization with the target's class,
606-- SPA version and windows, the pre-launch release, per launch the PCAS
607-- address, schedule and shader-cache invalidation (6 words), the final
608-- release -- the encoding the Coppelius GB10 runs execute. The compiler
609-- checks actual recipe lengths.
610def nvidiaSM121SubmissionBatchBytes = nvidiaSubmissionBatchBytes
611-- A batch of `launches` launches followed by another, as the backend places
612-- it: carrying its padding to the next 256-byte boundary
613-- (nativeEncodeNvidiaSubmissionPieces); the last batch has none.
614def nvidiaPaddedSubmissionBatchBytes = (lambda unrestricted launches : Nat .
615 (naturalMultiply (naturalDivideUnchecked (naturalAdd (nvidiaSubmissionBatchBytes launches) 255) 256) 256))
616-- `count` batches of `launches` launches each
617def nvidiaUniformSubmissionBatchesBytes = (lambda unrestricted count : Nat . (lambda unrestricted launches : Nat .
618 (naturalAdd (naturalMultiply (naturalSaturatingSubtract count 1) (nvidiaPaddedSubmissionBatchBytes launches))
619 (naturalSelect (naturalIsZero count) 0 (nvidiaSubmissionBatchBytes launches)))))
620
621
622def nvidiaLaunchScheduleCount =
623 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
624 (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule
625 (branch NvidiaLaunchScheduleEmpty . 0)
626 (branch NvidiaLaunchScheduleOne launch . 1)
627 (branch NvidiaLaunchScheduleAppend left right leftCount rightCount . (naturalAdd leftCount rightCount))
628 (branch NvidiaLaunchScheduleRepeat count iteration body bodyCount . (naturalMultiply count bodyCount))))
629
630-- Constant blocks have per-launch alignment. Derive their storage from the
631-- same schedule that supplies the launches, so a changed phase cannot leave
632-- an independently maintained count or byte capacity behind.
633def nvidiaLaunchParameterBytes =
634 (lambda unrestricted alignment : Nat . (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
635 (eliminate NvidiaLaunchTemplate (lambda unrestricted current : (family NvidiaLaunchTemplate) . Nat) launch
636 (branch NvidiaLaunchTemplateValue name kernel parameters .
637 (eliminate NvidiaLaunchKernel (lambda unrestricted current : (family NvidiaLaunchKernel) . Nat) kernel
638 (branch NvidiaLaunchKernelValue program x y z by bz bytes .
639 (naturalMultiply alignment
640 (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract alignment 1)) alignment))))))))
641def nvidiaLaunchScheduleParameterBytes =
642 (lambda unrestricted alignment : Nat . (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
643 (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule
644 (branch NvidiaLaunchScheduleEmpty . 0)
645 (branch NvidiaLaunchScheduleOne launch . (nvidiaLaunchParameterBytes alignment launch))
646 (branch NvidiaLaunchScheduleAppend left right leftBytes rightBytes . (naturalAdd leftBytes rightBytes))
647 (branch NvidiaLaunchScheduleRepeat count iteration body bodyBytes . (naturalMultiply count bodyBytes)))))
648
649-- Reserve exact per-launch constant extents after all canonical images.
650-- The backend may prune images but cannot require more code or parameter
651-- storage than this bound. Both terms come from the typed inputs it encodes.
652def nvidiaSM86ProgramCapacity =
653 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
654 (lambda unrestricted launches : (family NvidiaLaunchSchedule) .
655 (naturalAdd
656 (nvidiaCodeRegionExtent (nvidiaSM86RegionsPlacedEnd regions))
657 (nvidiaLaunchScheduleParameterBytes
658 nvidiaCodeRegionAlignment launches))))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.