1module Hardware.Nvidia.SM86.Command.WholeProgramPlan
2
3import Accelerator.SM86.Instruction
4import Accelerator.SM86.InstructionEncoding
5import Accelerator.SM86.Program
6import Accelerator.SM86.Operands
7import Hardware.Nvidia.SM86.Command.QMD
8import Std.Natural
9import Std.Foundation
10import Std.List
11import Data.Bytes
12import Model.Config
13import Model.Parameter
14import Model.Word64
15
16-- A program's machine code on a target that does not run its SM86 words
17-- (sm_121's: Accelerator.SM121.Lowering), or why it has none.
18family NvidiaDeviceRealization : Type 0
19constructor NvidiaDeviceRealized
20field unrestricted nvidiaDeviceRealizedMaterial : Bytes
21constructor NvidiaDeviceRealizationRefused
22field unrestricted nvidiaDeviceRealizationRefusal : Bytes
23end-family
24
25-- Target-owned, typed inputs to late NVIDIA component realization. These
26-- values remain ordinary Alpha data until whole-program erasure has selected a
27-- concrete target. `compiler-native-encode` is the backend boundary: it
28-- lowers this public representation without making a model own wire layouts.
29family NvidiaDeviceRegion : Type 0
30constructor NvidiaDeviceRegionValue
31field unrestricted nvidiaDeviceRegionIdentity : Bytes
32field unrestricted nvidiaDeviceRegionMaterial : Bytes
33field unrestricted nvidiaDeviceRegionRegisters : Nat
34field unrestricted nvidiaDeviceRegionBlockX : Nat
35field unrestricted nvidiaDeviceRegionSharedBytes : Nat
36-- SM121 needs an explicit barrier allocation. The older constructor cannot
37-- be silently reinterpreted as Blackwell: its resource contract lacks this
38-- field and its machine image belongs to another instruction profile.
39constructor NvidiaDeviceRegionSM121
40field unrestricted nvidiaSM121RegionIdentity : Bytes
41field unrestricted nvidiaSM121RegionMaterial : Bytes
42field unrestricted nvidiaSM121RegionRegisters : Nat
43field unrestricted nvidiaSM121RegionBlockX : Nat
44field unrestricted nvidiaSM121RegionSharedBytes : Nat
45field unrestricted nvidiaSM121RegionBarrierCount : Nat
46-- A region given as its typed SM86 program: its canonical placement is the
47-- program's SM86 encoding, and the backend places the machine code of the
48-- plan's target: the SM86 words, or the sm_121 realization (read only for an
49-- sm_121 plan).
50constructor NvidiaDeviceProgramRegion
51field unrestricted nvidiaDeviceProgramRegionIdentity : Bytes
52field unrestricted nvidiaDeviceProgramRegionProgram : (family SM86Program)
53field unrestricted nvidiaDeviceProgramRegionRegisters : Nat
54field unrestricted nvidiaDeviceProgramRegionBlockX : Nat
55field unrestricted nvidiaDeviceProgramRegionSharedBytes : Nat
56field unrestricted nvidiaDeviceProgramRegionSM121 : (family NvidiaDeviceRealization)
57-- a program region whose registers the compiler's backend allocates: the
58-- same instructions, order and control words, each value moved to the
59-- lowest aligned registers free over its live interval (the native
60-- encoder's nativeSM86AllocateProgram), and the demand the renumbered
61-- program declares; `registers` bounds it (the program as written)
62constructor NvidiaDeviceAllocatedProgramRegion
63field unrestricted nvidiaDeviceAllocatedProgramRegionIdentity : Bytes
64field unrestricted nvidiaDeviceAllocatedProgramRegionProgram : (family SM86Program)
65field unrestricted nvidiaDeviceAllocatedProgramRegionRegisters : Nat
66field unrestricted nvidiaDeviceAllocatedProgramRegionBlockX : Nat
67field unrestricted nvidiaDeviceAllocatedProgramRegionSharedBytes : Nat
68field unrestricted nvidiaDeviceAllocatedProgramRegionSM121 : (family NvidiaDeviceRealization)
69end-family
70
71family NvidiaDeviceRegions : Type 0
72constructor NvidiaDeviceRegionsEnd
73constructor NvidiaDeviceRegionsNext
74field unrestricted nvidiaDeviceRegionsHead : (family NvidiaDeviceRegion)
75recursive unrestricted nvidiaDeviceRegionsTail
76end-family
77
78-- Kernel parameters remain typed sparse words until late realization. The
79-- backend supplies zero-filled storage, checks every word offset against the
80-- launch's declared constant extent, and chooses the final program or spill
81-- address only after device-region erasure and compaction.
82family NvidiaParameterPatch : Type 0
83constructor NvidiaParameterPatchValue
84field unrestricted nvidiaParameterPatchWordOffset : Nat
85field unrestricted nvidiaParameterPatchWordValue : (family ModelWord64)
86end-family
87
88family NvidiaParameterPatches : Type 0
89constructor NvidiaParameterPatchesEnd
90constructor NvidiaParameterPatchesNext
91field unrestricted nvidiaParameterPatchesHead : (family NvidiaParameterPatch)
92recursive unrestricted nvidiaParameterPatchesTail
93end-family
94
95family NvidiaParameterBlock : Type 0
96constructor NvidiaParameterBlockValue
97field unrestricted nvidiaParameterBlockPatches : (family NvidiaParameterPatches)
98end-family
99
100-- Repeat adjustments name a block ordinal within the expanded repeated body,
101-- or every block when one training scalar is shared by a phase. Affine and
102-- quotient/remainder adjustments are deltas; table frames are exact values.
103family NvidiaParameterAdjustmentScope : Type 0
104constructor NvidiaParameterAdjustmentAllBlocks
105constructor NvidiaParameterAdjustmentBlock
106field unrestricted nvidiaParameterAdjustmentBlockOrdinal : Nat
107end-family
108
109family NvidiaParameterAdjustment : Type 0
110constructor NvidiaParameterAdjustmentValue
111field unrestricted nvidiaParameterAdjustmentScope : (family NvidiaParameterAdjustmentScope)
112field unrestricted nvidiaParameterAdjustmentWordOffset : Nat
113field unrestricted nvidiaParameterAdjustmentWordValue : (family ModelWord64)
114end-family
115
116family NvidiaParameterAdjustments : Type 0
117constructor NvidiaParameterAdjustmentsEnd
118constructor NvidiaParameterAdjustmentsNext
119field unrestricted nvidiaParameterAdjustmentsHead : (family NvidiaParameterAdjustment)
120recursive unrestricted nvidiaParameterAdjustmentsTail
121end-family
122
123family NvidiaParameterAdjustmentFrames : Type 0
124constructor NvidiaParameterAdjustmentFramesEnd
125constructor NvidiaParameterAdjustmentFramesNext
126field unrestricted nvidiaParameterAdjustmentFrame : (family NvidiaParameterAdjustments)
127recursive unrestricted nvidiaParameterAdjustmentFramesTail
128end-family
129
130family NvidiaParameterIteration : Type 0
131constructor NvidiaParameterIterationUnchanged
132constructor NvidiaParameterIterationAffine
133field unrestricted nvidiaParameterIterationAffineDeltas : (family NvidiaParameterAdjustments)
134constructor NvidiaParameterIterationQuotientRemainder
135field unrestricted nvidiaParameterIterationDivisor : Nat
136field unrestricted nvidiaParameterIterationRemainderDeltas : (family NvidiaParameterAdjustments)
137field unrestricted nvidiaParameterIterationQuotientDeltas : (family NvidiaParameterAdjustments)
138constructor NvidiaParameterIterationTable
139field unrestricted nvidiaParameterIterationFrames : (family NvidiaParameterAdjustmentFrames)
140end-family
141
142-- A launch names a typed device region by its pre-compaction address and
143-- carries only semantic launch geometry and constant-buffer placement. Code
144-- extent, prefetch width, block X, register count and shared memory are
145-- deliberately absent: the backend derives those fields from the retained
146-- device region after whole-program erasure.
147family NvidiaLaunchKernel : Type 0
148constructor NvidiaLaunchKernelValue
149field unrestricted nvidiaLaunchProgramAddress : (family ModelWord64)
150field unrestricted nvidiaLaunchGridX : Nat
151field unrestricted nvidiaLaunchGridY : Nat
152field unrestricted nvidiaLaunchGridZ : Nat
153field unrestricted nvidiaLaunchBlockY : Nat
154field unrestricted nvidiaLaunchBlockZ : Nat
155field unrestricted nvidiaLaunchConstantBytes : Nat
156end-family
157
158family NvidiaLaunchTemplate : Type 0
159constructor NvidiaLaunchTemplateValue
160field unrestricted nvidiaLaunchSourceIdentity : Bytes
161field unrestricted nvidiaLaunchKernel : (family NvidiaLaunchKernel)
162field unrestricted nvidiaLaunchParameters : (family NvidiaParameterBlock)
163end-family
164
165-- Repeated training phases stay compact in source. Parameter iteration
166-- metadata transforms sparse words without duplicating parameter blocks,
167-- device images or descriptor bytes in the checked graph.
168family NvidiaLaunchSchedule : Type 0
169constructor NvidiaLaunchScheduleEmpty
170constructor NvidiaLaunchScheduleOne
171field unrestricted nvidiaLaunchScheduleLaunch : (family NvidiaLaunchTemplate)
172constructor NvidiaLaunchScheduleAppend
173recursive unrestricted nvidiaLaunchScheduleLeft
174recursive unrestricted nvidiaLaunchScheduleRight
175constructor NvidiaLaunchScheduleRepeat
176field unrestricted nvidiaLaunchScheduleRepeatCount : Nat
177field unrestricted nvidiaLaunchScheduleParameterIteration : (family NvidiaParameterIteration)
178recursive unrestricted nvidiaLaunchScheduleRepeatedBody
179end-family
180
181-- Submission ranges refer to ordinals in the realized QMD table. Pushbuffer
182-- methods and GPFIFO entries are derived from these ranges after launch
183-- erasure; neither their addresses nor padding are frozen in model source.
184family NvidiaLaunchReferences : Type 0
185constructor NvidiaLaunchReferencesEmpty
186constructor NvidiaLaunchReferencesRange
187field unrestricted nvidiaLaunchReferenceFirst : Nat
188field unrestricted nvidiaLaunchReferenceCount : Nat
189constructor NvidiaLaunchReferencesAppend
190recursive unrestricted nvidiaLaunchReferencesLeft
191recursive unrestricted nvidiaLaunchReferencesRight
192end-family
193
194family NvidiaSubmissionBatch : Type 0
195constructor NvidiaSubmissionBatchValue
196field unrestricted nvidiaSubmissionSourceIdentity : Bytes
197field unrestricted nvidiaSubmissionSemaphoreOffset : Nat
198field unrestricted nvidiaSubmissionReferences : (family NvidiaLaunchReferences)
199end-family
200
201family NvidiaSubmissionSchedule : Type 0
202constructor NvidiaSubmissionScheduleEmpty
203constructor NvidiaSubmissionScheduleOne
204field unrestricted nvidiaSubmissionScheduleBatch : (family NvidiaSubmissionBatch)
205constructor NvidiaSubmissionScheduleAppend
206recursive unrestricted nvidiaSubmissionScheduleLeft
207recursive unrestricted nvidiaSubmissionScheduleRight
208constructor NvidiaSubmissionScheduleRepeat
209field unrestricted nvidiaSubmissionScheduleRepeatCount : Nat
210field unrestricted nvidiaSubmissionReferenceStride : Nat
211field unrestricted nvidiaSubmissionSemaphoreStride : Nat
212recursive unrestricted nvidiaSubmissionScheduleRepeatedBody
213-- The same submissions, each launch followed by a semaphore release that
214-- waits for it to finish and carries the device's timestamp, at `offset` +
215-- 16 x the launch's QMD ordinal from the plan's semaphore base (its payload
216-- the ordinal): the device time of every launch, for a profile. Waiting for
217-- each launch serializes launches the plan would otherwise let overlap, so a
218-- profile's step is not the production step's time.
219constructor NvidiaSubmissionScheduleProfiled
220field unrestricted nvidiaSubmissionProfileOffset : Nat
221recursive unrestricted nvidiaSubmissionProfiledBody
222end-family
223
224family NvidiaQMDRecipeBlocks : Type 0
225constructor NvidiaQMDRecipeBlocksEnd
226constructor NvidiaQMDRecipeBlocksNext
227field unrestricted nvidiaQMDRecipeBlockIdentity : Bytes
228field unrestricted nvidiaQMDRecipeBlockOutputBytes : (family ModelWord64)
229field unrestricted nvidiaQMDRecipeBlockRecordCount : Nat
230field unrestricted nvidiaQMDRecipeBlockZeroRecords : Nat
231field unrestricted nvidiaQMDRecipeBlockRecords : Bytes
232recursive unrestricted nvidiaQMDRecipeBlocksTail
233end-family
234
235family NvidiaPackbitsRecipeBlocks : Type 0
236constructor NvidiaPackbitsRecipeBlocksEnd
237constructor NvidiaPackbitsRecipeBlocksNext
238field unrestricted nvidiaPackbitsRecipeBlockIdentity : Bytes
239field unrestricted nvidiaPackbitsRecipeBlockOutputBytes : (family ModelWord64)
240field unrestricted nvidiaPackbitsRecipeBlockCommandCount : Nat
241field unrestricted nvidiaPackbitsRecipeBlockBytes : Bytes
242recursive unrestricted nvidiaPackbitsRecipeBlocksTail
243end-family
244
245family NvidiaPushRecipeBlocks : Type 0
246constructor NvidiaPushRecipeBlocksEnd
247constructor NvidiaPushRecipeBlocksNext
248field unrestricted nvidiaPushRecipeBlockPushIdentity : Bytes
249field unrestricted nvidiaPushRecipeBlockPushBytes : (family ModelWord64)
250field unrestricted nvidiaPushRecipeBlockGPFIFOIdentity : Bytes
251field unrestricted nvidiaPushRecipeBlockGPFIFOBytes : (family ModelWord64)
252field unrestricted nvidiaPushRecipeBlockBatchCount : Nat
253field unrestricted nvidiaPushRecipeBlockBatches : Bytes
254recursive unrestricted nvidiaPushRecipeBlocksTail
255end-family
256
257family NvidiaPhysicalComponentPlan : Type 0
258constructor NvidiaProgramComponentPlan
259field unrestricted nvidiaProgramImages : Bytes
260field unrestricted nvidiaProgramImageCursor : Nat
261field unrestricted nvidiaProgramImageCount : Nat
262field unrestricted nvidiaProgramExpectedImageCursor : Nat
263field unrestricted nvidiaProgramExpectedImageCount : Nat
264field unrestricted nvidiaProgramGapBytes : Nat
265field unrestricted nvidiaProgramRecipeCommands : Nat
266field unrestricted nvidiaProgramRecipe : Bytes
267field unrestricted nvidiaProgramRecipeDropBytes : Nat
268field unrestricted nvidiaProgramOutputBytes : Nat
269constructor NvidiaQMDComponentPlan
270field unrestricted nvidiaQMDArchitecture : (family ModelWord32)
271field unrestricted nvidiaQMDBlocks : (family NvidiaQMDRecipeBlocks)
272constructor NvidiaPackbitsComponentPlan
273field unrestricted nvidiaPackbitsPrefixZeroBytes : Nat
274field unrestricted nvidiaPackbitsBlocks : (family NvidiaPackbitsRecipeBlocks)
275constructor NvidiaPushComponentPlan
276field unrestricted nvidiaPushComputeClass : (family ModelWord32)
277field unrestricted nvidiaPushSPAVersion : (family ModelWord32)
278field unrestricted nvidiaPushBlocks : (family NvidiaPushRecipeBlocks)
279constructor NvidiaGPFIFOComponentPlan
280field unrestricted nvidiaGPFIFOComputeClass : (family ModelWord32)
281field unrestricted nvidiaGPFIFOSPAVersion : (family ModelWord32)
282field unrestricted nvidiaGPFIFOBlocks : (family NvidiaPushRecipeBlocks)
283end-family
284
285-- One connected late-realization plan. Program compaction and QMD rewriting
286-- consume this value together, so a descriptor cannot retain an address or a
287-- resource count from an erased or superseded device region. The historical
288-- recipe parameter offset and component capacity are compatibility bounds for
289-- the current host protocol, not output-layout requirements: retained images
290-- are repacked and their QMD fields are derived again before the component is
291-- padded to the admitted arena capacity.
292family NvidiaWholeProgramComponent : Type 0
293constructor NvidiaWholeProgramProgram
294constructor NvidiaWholeProgramQMD
295constructor NvidiaWholeProgramPushbuffer
296constructor NvidiaWholeProgramGPFIFO
297-- The same four tables as launch-table recipes: the compact form the host
298-- expands into the mapped arena at startup with the shared
299-- Runtime.NativeLaunchRecipeRoutine. The compiler derives each recipe from
300-- the schedule's repeat structure and publishes it only after it has expanded
301-- it back to the exact table bytes.
302constructor NvidiaWholeProgramProgramRecipe
303constructor NvidiaWholeProgramQMDRecipe
304constructor NvidiaWholeProgramPushbufferRecipe
305constructor NvidiaWholeProgramGPFIFORecipe
306-- The device address of each launch's parameter block, in launch order (a
307-- little-endian u64 each), as the realization placed it: in the program
308-- region after the retained code, or past the QMD table. A host that
309-- supplies a parameter word at run time writes it there.
310constructor NvidiaWholeProgramParameterAddresses
311-- The 8-byte word at a byte offset of each launch's parameter block, in
312-- launch order, as realized (0 past the block's extent): what a host that
313-- supplies a word at run time checks its sites against.
314constructor NvidiaWholeProgramParameterWords
315field unrestricted nvidiaWholeProgramParameterWordOffset : Nat
316-- The launch manifest, one text line per launch in QMD order: the ordinal,
317-- the launch's source identity and its device region's identity, separated
318-- by tabs. A per-launch profile (NvidiaSubmissionScheduleProfiled) records
319-- one stamp per QMD ordinal; the manifest names what each ordinal ran.
320constructor NvidiaWholeProgramLaunchIdentities
321end-family
322
323family NvidiaWholeProgramPlan : Type 0
324constructor NvidiaWholeProgramPlanValue
325field unrestricted nvidiaWholeProgramComponent : (family NvidiaWholeProgramComponent)
326field unrestricted nvidiaWholeProgramArchitecture : (family ModelWord32)
327field unrestricted nvidiaWholeProgramComputeClass : (family ModelWord32)
328field unrestricted nvidiaWholeProgramSPAVersion : (family ModelWord32)
329field unrestricted nvidiaWholeProgramProgramBase : (family ModelWord64)
330field unrestricted nvidiaWholeProgramQMDBase : (family ModelWord64)
331field unrestricted nvidiaWholeProgramPushbufferBase : (family ModelWord64)
332field unrestricted nvidiaWholeProgramSemaphoreBase : (family ModelWord64)
333field unrestricted nvidiaWholeProgramRegionAlignment : Nat
334field unrestricted nvidiaWholeProgramProgramCapacity : Nat
335field unrestricted nvidiaWholeProgramRegions : (family NvidiaDeviceRegions)
336field unrestricted nvidiaWholeProgramLaunchSchedule : (family NvidiaLaunchSchedule)
337field unrestricted nvidiaWholeProgramExpectedLaunchCount : Nat
338field unrestricted nvidiaWholeProgramQMDTableBytes : Nat
339field unrestricted nvidiaWholeProgramSubmissions : (family NvidiaSubmissionSchedule)
340field unrestricted nvidiaWholeProgramExpectedSubmissionCount : Nat
341field unrestricted nvidiaWholeProgramExpectedReferenceCount : Nat
342end-family
343
344family NvidiaSubmissionByteShape : Type 0
345constructor NvidiaSubmissionByteShapeValue
346field unrestricted nvidiaSubmissionPaddedBytes : Nat
347field unrestricted nvidiaSubmissionFinalPadding : Nat
348end-family
349
350
351def nvidiaLaunchFirstOrdinal : Nat = 0
352def nvidiaSubmissionFirstSemaphoreOffset : Nat = 0
353
354def nvidiaLaunchReferencesCount =
355 (lambda unrestricted references : (family NvidiaLaunchReferences) .
356 (eliminate NvidiaLaunchReferences
357 (lambda unrestricted current : (family NvidiaLaunchReferences) . Nat)
358 references
359 (branch NvidiaLaunchReferencesEmpty . 0)
360 (branch NvidiaLaunchReferencesRange first count . count)
361 (branch NvidiaLaunchReferencesAppend left right leftCount rightCount .
362 (naturalAdd leftCount rightCount))))
363def nvidiaSubmissionScheduleCount =
364 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
365 (eliminate NvidiaSubmissionSchedule
366 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
367 schedule
368 (branch NvidiaSubmissionScheduleEmpty . 0)
369 (branch NvidiaSubmissionScheduleOne batch . 1)
370 (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount .
371 (naturalAdd leftCount rightCount))
372 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount .
373 (naturalMultiply count bodyCount))
374 (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount)))
375def nvidiaSubmissionScheduleReferenceCount =
376 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
377 (eliminate NvidiaSubmissionSchedule
378 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
379 schedule
380 (branch NvidiaSubmissionScheduleEmpty . 0)
381 (branch NvidiaSubmissionScheduleOne batch .
382 (eliminate NvidiaSubmissionBatch
383 (lambda unrestricted current : (family NvidiaSubmissionBatch) . Nat)
384 batch
385 (branch NvidiaSubmissionBatchValue identity semaphore references .
386 (nvidiaLaunchReferencesCount references))))
387 (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount .
388 (naturalAdd leftCount rightCount))
389 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount .
390 (naturalMultiply count bodyCount))
391 (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount)))
392
393-- Four 32-bit words carry a release payload and its device timestamp. The
394-- profiled schedule indexes these slots by the whole plan's QMD ordinal.
395def nvidiaSubmissionProfileSlotBytes : Nat = 16
396
397def nvidiaSubmissionHasProfile =
398 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
399 (eliminate NvidiaSubmissionSchedule
400 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
401 schedule
402 (branch NvidiaSubmissionScheduleEmpty . 0)
403 (branch NvidiaSubmissionScheduleOne batch . 0)
404 (branch NvidiaSubmissionScheduleAppend left right leftProfile rightProfile .
405 (naturalNonzero (naturalAdd leftProfile rightProfile)))
406 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyProfile .
407 (naturalAnd (naturalNonzero count) bodyProfile))
408 (branch NvidiaSubmissionScheduleProfiled offset body bodyProfile .
409 (naturalNonzero (nvidiaSubmissionScheduleReferenceCount body)))))
410
411-- Derive the semaphore arena from addressed slots, rather than submission
412-- count. A profiled graph adds device-timer slots beyond ordinary completion
413-- slots; repeated bodies may have explicit holes or a nonzero first slot.
414-- launchCount bounds QMD ordinals, including prefixes not being profiled.
415def nvidiaSubmissionSemaphoreExtent =
416 (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
417 (lambda unrestricted completionSlotBytes : Nat .
418 (lambda unrestricted launchCount : Nat .
419 (eliminate NvidiaSubmissionSchedule
420 (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat)
421 schedule
422 (branch NvidiaSubmissionScheduleEmpty . 0)
423 (branch NvidiaSubmissionScheduleOne batch .
424 (eliminate NvidiaSubmissionBatch
425 (lambda unrestricted current : (family NvidiaSubmissionBatch) . Nat)
426 batch
427 (branch NvidiaSubmissionBatchValue identity offset references .
428 (naturalAdd offset completionSlotBytes))))
429 (branch NvidiaSubmissionScheduleAppend left right leftExtent rightExtent .
430 (naturalAdd leftExtent (naturalSaturatingSubtract rightExtent leftExtent)))
431 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyExtent .
432 (naturalMultiply (naturalAnd (naturalNonzero count) (naturalNonzero bodyExtent))
433 (naturalAdd bodyExtent
434 (naturalMultiply (naturalSaturatingSubtract count 1) semaphoreStride))))
435 (branch NvidiaSubmissionScheduleProfiled offset body bodyExtent .
436 (naturalAdd bodyExtent
437 (naturalSaturatingSubtract
438 (naturalMultiply (naturalNonzero (nvidiaSubmissionScheduleReferenceCount body))
439 (naturalAdd offset (naturalMultiply nvidiaSubmissionProfileSlotBytes launchCount)))
440 bodyExtent)))))))
441
442-- Versioned bounded descriptor consumed by `alpha observe import
443-- launch-profile`. Identities come from NvidiaWholeProgramLaunchIdentities,
444-- preserving the compiler's QMD order and submission membership.
445def nvidiaLaunchProfileManifestAdmitted =
446 (lambda unrestricted launches : Nat .
447 (lambda unrestricted submissions : Nat .
448 (lambda unrestricted stride : Nat .
449 (lambda unrestricted fromEnd : Nat .
450 (lambda unrestricted offset : Nat .
451 (naturalAnd
452 (naturalAnd (naturalLess launches (naturalPowerOfTwo 64))
453 (naturalLess submissions (naturalPowerOfTwo 64)))
454 (naturalAnd
455 (naturalAnd (naturalLess stride (naturalPowerOfTwo 64))
456 (naturalLess fromEnd (naturalPowerOfTwo 64)))
457 (naturalAnd (naturalLess offset (naturalPowerOfTwo 64))
458 (naturalAnd (naturalLessOrEqual 32 stride)
459 (naturalAnd
460 (naturalLessOrEqual (naturalMultiply stride submissions) offset)
461 (naturalLessOrEqual
462 (naturalAdd offset (naturalMultiply nvidiaSubmissionProfileSlotBytes launches))
463 fromEnd)))))))))))
464
465def nvidiaLaunchProfileManifest =
466 (lambda unrestricted launches : Nat .
467 (lambda unrestricted submissions : Nat .
468 (lambda unrestricted stride : Nat .
469 (lambda unrestricted fromEnd : Nat .
470 (lambda unrestricted offset : Nat .
471 (lambda unrestricted identities : Bytes .
472 (lambda erased admitted :
473 (equal Nat (nvidiaLaunchProfileManifestAdmitted launches submissions stride fromEnd offset) 1) .
474 (bytes-append b"ALPXPRF1"
475 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated launches))
476 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated submissions))
477 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated stride))
478 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated fromEnd))
479 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated offset))
480 (bytes-append (dataBytesWord64LE (modelWord64FromNaturalTruncated nvidiaSubmissionProfileSlotBytes))
481 identities))))))))))))))
482
483-- A launch can declare ordered, typed patches without nesting one constructor
484-- per ABI argument. Validation of offsets and extent still belongs to the
485-- late parameter-block realization, after image pruning and placement.
486def nvidiaParameterPatchesFromList =
487 (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) .
488 (eliminate StdList
489 (lambda unrestricted current : (family StdList (family NvidiaParameterPatch)) .
490 (family NvidiaParameterPatches))
491 patches
492 (branch StdListEmpty .
493 (constructor NvidiaParameterPatches NvidiaParameterPatchesEnd))
494 (branch StdListCons head tail induction .
495 (constructor NvidiaParameterPatches NvidiaParameterPatchesNext
496 head induction))))
497def nvidiaParameterBlockFromList =
498 (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) .
499 (constructor NvidiaParameterBlock NvidiaParameterBlockValue
500 (nvidiaParameterPatchesFromList patches)))
501
502-- A layer may reuse the same typed image and launch geometry while its
503-- parameter pointers change. Keeping identity and kernel together prevents
504-- callers from restating hardware launch facts for each layer.
505def nvidiaLaunchWithParameters =
506 (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
507 (lambda unrestricted parameters : (family NvidiaParameterBlock) .
508 (eliminate NvidiaLaunchTemplate
509 (lambda unrestricted current : (family NvidiaLaunchTemplate) .
510 (family NvidiaLaunchTemplate)) launch
511 (branch NvidiaLaunchTemplateValue identity kernel previous .
512 (constructor NvidiaLaunchTemplate NvidiaLaunchTemplateValue
513 identity kernel parameters)))))
514def nvidiaLaunchSequence =
515 (lambda unrestricted launches : (family StdList (family NvidiaLaunchTemplate)) .
516 (stdListFold (family NvidiaLaunchTemplate) (family NvidiaLaunchSchedule)
517 (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
518 (lambda unrestricted tail : (family NvidiaLaunchSchedule) .
519 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleAppend
520 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleOne launch) tail)))
521 (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleEmpty) launches))
522
523-- CB0 uses 64-bit pointer slots after the target QMD parameter header.
524-- Systems supply addresses from their arena layout, not literal word slots.
525def nvidiaKernelBlockXWord : Nat =
526 (naturalDivideUnchecked qmdBlockDimensionXOffset 8)
527def nvidiaKernelPointerSlotBytes : Nat = 8
528def nvidiaKernelPointerByteOffset =
529 (lambda unrestricted argument : Nat .
530 (naturalAdd qmdKernelParameterBase
531 (naturalMultiply nvidiaKernelPointerSlotBytes argument)))
532def nvidiaKernelPointerWord =
533 (lambda unrestricted argument : Nat .
534 (naturalDivideUnchecked (nvidiaKernelPointerByteOffset argument)
535 nvidiaKernelPointerSlotBytes))
536def nvidiaKernelPointerPatch =
537 (lambda unrestricted argument : Nat . (lambda unrestricted address : Nat .
538 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
539 (nvidiaKernelPointerWord argument)
540 (modelWord64FromNaturalTruncated address))))
541def nvidiaKernelU32WordPatch =
542 (lambda unrestricted slot : Nat . (lambda unrestricted word : Nat .
543 (lambda erased admitted :
544 (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) .
545 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
546 slot (modelWord64FromNaturalTruncated word)))))
547-- Two neighboring 32-bit CB0 scalars share one 64-bit sparse patch. Packing
548-- them here prevents a later patch from overwriting the first scalar.
549def nvidiaKernelU32PairPatch =
550 (lambda unrestricted argument : Nat .
551 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
552 (lambda erased lowAdmitted :
553 (equal Nat (naturalLess low (naturalPowerOfTwo 32)) 1) .
554 (lambda erased highAdmitted :
555 (equal Nat (naturalLess high (naturalPowerOfTwo 32)) 1) .
556 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
557 (nvidiaKernelPointerWord argument)
558 (modelWord64FromNaturalTruncated
559 (naturalAdd low (naturalMultiply high (naturalPowerOfTwo 32))))))))))
560-- A whole-table certificate admits dynamic indices whose selected values
561-- cannot be reduced while checking a launch-construction lambda. An index
562-- beyond the list yields zero; the schedule owner separately proves length.
563def nvidiaKernelU32TableOverflowCount =
564 (lambda unrestricted table : (family StdList Nat) .
565 (stdListFold Nat Nat
566 (lambda unrestricted word : Nat . (lambda unrestricted count : Nat .
567 (naturalAdd count
568 (naturalSelect (naturalLess word (naturalPowerOfTwo 32)) 0 1))))
569 0 table))
570def nvidiaKernelU32TableWordAt =
571 (lambda unrestricted table : (family StdList Nat) .
572 (lambda unrestricted index : Nat .
573 (stdOptionValueOr Nat 0 (stdListIndex Nat table index))))
574def nvidiaKernelU32PairPatchFromCertifiedTable =
575 (lambda unrestricted argument : Nat .
576 (lambda unrestricted table : (family StdList Nat) .
577 (lambda unrestricted index : Nat .
578 (lambda erased admitted :
579 (equal Nat (nvidiaKernelU32TableOverflowCount table) 0) .
580 (constructor NvidiaParameterPatch NvidiaParameterPatchValue
581 (nvidiaKernelPointerWord argument)
582 (modelWord64FromNaturalTruncated
583 (naturalAdd
584 (nvidiaKernelU32TableWordAt table index)
585 (naturalMultiply
586 (nvidiaKernelU32TableWordAt table (succ index))
587 (naturalPowerOfTwo 32)))))))))
588def nvidiaKernelF32ScalarPatch =
589 (lambda unrestricted argument : Nat . (lambda unrestricted word : Nat .
590 (lambda erased admitted :
591 (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) .
592 (nvidiaKernelU32WordPatch
593 (nvidiaKernelPointerWord argument) word admitted))))
594
595-- Compose independently owned device closures before whole-program pruning.
596-- This preserves order; placement and duplicate-identity admission remain
597-- the whole-program planner's responsibility.
598def nvidiaAppendDeviceRegions =
599 (lambda unrestricted left : (family NvidiaDeviceRegions) .
600 (lambda unrestricted right : (family NvidiaDeviceRegions) .
601 (eliminate NvidiaDeviceRegions
602 (lambda unrestricted current : (family NvidiaDeviceRegions) . (family NvidiaDeviceRegions)) left
603 (branch NvidiaDeviceRegionsEnd . right)
604 (branch NvidiaDeviceRegionsNext head tail induction .
605 (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext head induction)))))
606
607-- how many launches a schedule expands to
608-- Extents of the v1 submission protocol used by the backend: initialization
609-- has four two-word methods, three three-word methods, and 64 two-word CWD
610-- counter methods. Each of the two semaphore releases is six words; a launch
611-- is three two-word methods. Keep sizing separate from byte encoding so a
612-- placement proof need not normalize a machine image. Artifact gates compare
613-- this extent with the backend's actual output before accepting the image.
614def nvidiaCodeRegionAlignment : Nat = 256
615def nvidiaCodeRegionExtent = (lambda unrestricted bytes : Nat .
616 (naturalMultiply nvidiaCodeRegionAlignment
617 (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1)) nvidiaCodeRegionAlignment)))
618-- SM86 placement uses the same 256-byte alignment and 16-byte instruction
619-- extent as nativePlaceNvidiaRegions. A target-specific lookup is required:
620-- SM121 lowering can change a typed program's byte extent.
621def nvidiaSM86RegionIdentity =
622 (lambda unrestricted region : (family NvidiaDeviceRegion) .
623 (eliminate NvidiaDeviceRegion
624 (lambda unrestricted current : (family NvidiaDeviceRegion) . Bytes) region
625 (branch NvidiaDeviceRegionValue identity material registers block shared . identity)
626 (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . identity)
627 (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget . identity)
628 (branch NvidiaDeviceAllocatedProgramRegion identity program registers block shared otherTarget . identity)))
629def nvidiaSM86RegionExtent =
630 (lambda unrestricted region : (family NvidiaDeviceRegion) .
631 (eliminate NvidiaDeviceRegion
632 (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region
633 (branch NvidiaDeviceRegionValue identity material registers block shared . (bytes-length material))
634 (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . 0)
635 (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget .
636 (naturalMultiply sm86InstructionBytes (sm86ProgramCount program)))
637 (branch NvidiaDeviceAllocatedProgramRegion identity program registers block shared otherTarget .
638 (naturalMultiply sm86InstructionBytes (sm86ProgramCount program)))))
639def nvidiaSM86RegionsAdmitted =
640 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
641 (eliminate NvidiaDeviceRegions
642 (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
643 (branch NvidiaDeviceRegionsEnd . 1)
644 (branch NvidiaDeviceRegionsNext head tail induction .
645 (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head)) induction))))
646-- The end of the canonical region placement, before reachability pruning.
647-- A program arena sized from this upper bound remains valid when a launch
648-- disappears or code is compacted; each region starts at the same alignment
649-- nativePlaceNvidiaRegions uses for SM86.
650def nvidiaSM86RegionsPlacedEnd =
651 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
652 (app
653 (eliminate NvidiaDeviceRegions
654 (lambda unrestricted current : (family NvidiaDeviceRegions) .
655 (pi unrestricted cursor : Nat . Nat)) regions
656 (branch NvidiaDeviceRegionsEnd .
657 (lambda unrestricted cursor : Nat . cursor))
658 (branch NvidiaDeviceRegionsNext head tail induction .
659 (lambda unrestricted cursor : Nat .
660 (induction (naturalAdd (nvidiaCodeRegionExtent cursor)
661 (nvidiaSM86RegionExtent head))))))
662 0))
663def nvidiaSM86RegionPrefixAdmitted =
664 (lambda unrestricted identity : Bytes .
665 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
666 (eliminate NvidiaDeviceRegions
667 (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions
668 (branch NvidiaDeviceRegionsEnd . 0)
669 (branch NvidiaDeviceRegionsNext head tail induction .
670 (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head))
671 (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity)
672 1 induction))))))
673def nvidiaSM86RegionOffsetFrom =
674 (lambda unrestricted identity : Bytes .
675 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
676 (eliminate NvidiaDeviceRegions
677 (lambda unrestricted current : (family NvidiaDeviceRegions) . (pi unrestricted cursor : Nat . Nat)) regions
678 (branch NvidiaDeviceRegionsEnd . (lambda unrestricted cursor : Nat . 0))
679 (branch NvidiaDeviceRegionsNext head tail induction .
680 (lambda unrestricted cursor : Nat .
681 (let unrestricted placed = (nvidiaCodeRegionExtent cursor) in
682 (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity)
683 placed
684 (induction (naturalAdd placed (nvidiaSM86RegionExtent head))))))))))
685def nvidiaSM86RegionAddressAdmitted =
686 (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes .
687 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
688 (naturalAnd (naturalNonzero base)
689 (naturalAnd (naturalIsZero (naturalModuloUnchecked base nvidiaCodeRegionAlignment))
690 (nvidiaSM86RegionPrefixAdmitted identity regions))))))
691def nvidiaSM86RegionAddress =
692 (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes .
693 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
694 (lambda erased admitted :
695 (equal Nat (nvidiaSM86RegionAddressAdmitted base identity regions) 1) .
696 (naturalAdd base (nvidiaSM86RegionOffsetFrom identity regions 0))))))
697-- CB0 extents are rounded to QMD's sixteen-byte size unit, independently
698-- of the stronger alignment imposed on the parameter block's device VA.
699def nvidiaKernelConstantExtentUnit : Nat = 16
700def nvidiaKernelConstantExtent = (lambda unrestricted argumentEnd : Nat .
701 (naturalMultiply nvidiaKernelConstantExtentUnit
702 (naturalDivideUnchecked (naturalAdd argumentEnd (naturalSaturatingSubtract nvidiaKernelConstantExtentUnit 1))
703 nvidiaKernelConstantExtentUnit)))
704def nvidiaSM121ConstantExtentUnit : Nat = nvidiaKernelConstantExtentUnit
705def nvidiaSM121ConstantExtent = nvidiaKernelConstantExtent
706def nvidiaSM121QMDRecordBytes : Nat = (naturalMultiply 96 4)
707def nvidiaSM121QMDSlotBytes : Nat =
708 (naturalMultiply nvidiaCodeRegionAlignment
709 (naturalDivideUnchecked (naturalAdd nvidiaSM121QMDRecordBytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1))
710 nvidiaCodeRegionAlignment))
711def nvidiaSubmissionWordBytes : Nat = 4
712-- A submission's semaphore release is one method header and five operands:
713-- two address words, payload, upper payload, operation. The encoder's plain
714-- batch emits a pre-release and a final release; a profiled batch additionally
715-- emits one after each referenced launch. ProfiledSubmissionContract holds
716-- the actual native bytes to Pushbuffer's release owner.
717def nvidiaSubmissionReleaseBytes : Nat =
718 (naturalMultiply nvidiaSubmissionWordBytes 6)
719def nvidiaSubmissionBatchBytes = (lambda unrestricted launches : Nat .
720 (naturalMultiply nvidiaSubmissionWordBytes
721 (naturalAdd (naturalAdd (naturalMultiply 2 (naturalAdd 4 64)) (naturalMultiply 3 3))
722 (naturalAdd (naturalMultiply 2 (naturalDivideUnchecked nvidiaSubmissionReleaseBytes nvidiaSubmissionWordBytes)) (naturalMultiply launches (naturalMultiply 3 2))))))
723-- A Blackwell batch is encoded as an Ampere one (the backend's
724-- nativeEncodeNvidiaSubmissionPieces, one target abstraction since the
725-- 2026-09-26 merge): the compute initialization with the target's class,
726-- SPA version and windows, the pre-launch release, per launch the PCAS
727-- address, schedule and shader-cache invalidation (6 words), the final
728-- release -- the encoding the Coppelius GB10 runs execute. The compiler
729-- checks actual recipe lengths.
730def nvidiaSM121SubmissionBatchBytes = nvidiaSubmissionBatchBytes
731-- A batch of `launches` launches followed by another, as the backend places
732-- it: carrying its padding to the next 256-byte boundary
733-- (nativeEncodeNvidiaSubmissionPieces); the last batch has none.
734def nvidiaPaddedSubmissionBatchBytes = (lambda unrestricted launches : Nat .
735 (naturalMultiply (naturalDivideUnchecked (naturalAdd (nvidiaSubmissionBatchBytes launches) 255) 256) 256))
736-- `count` batches of `launches` launches each
737def nvidiaUniformSubmissionBatchesBytes = (lambda unrestricted count : Nat . (lambda unrestricted launches : Nat .
738 (naturalAdd (naturalMultiply (naturalSaturatingSubtract count 1) (nvidiaPaddedSubmissionBatchBytes launches))
739 (naturalSelect (naturalIsZero count) 0 (nvidiaSubmissionBatchBytes launches)))))
740
741-- Carry padding and the last batch's removable tail together. Appending a
742-- nonempty right schedule makes the left tail internal; an empty right or a
743-- zero repeat cannot remove the real last batch's padding. Sizes depend on
744-- references and profiling, never addresses or a fixed allocation allowance.
745def nvidiaSubmissionPaddedBytesOf = (lambda unrestricted shape : (family NvidiaSubmissionByteShape) .
746 (eliminate NvidiaSubmissionByteShape (lambda unrestricted current : (family NvidiaSubmissionByteShape) . Nat)
747 shape (branch NvidiaSubmissionByteShapeValue padded padding . padded)))
748def nvidiaSubmissionFinalPaddingOf = (lambda unrestricted shape : (family NvidiaSubmissionByteShape) .
749 (eliminate NvidiaSubmissionByteShape (lambda unrestricted current : (family NvidiaSubmissionByteShape) . Nat)
750 shape (branch NvidiaSubmissionByteShapeValue padded padding . padding)))
751def nvidiaSubmissionByteShapeAppend = (lambda unrestricted left : (family NvidiaSubmissionByteShape) .
752 (lambda unrestricted right : (family NvidiaSubmissionByteShape) .
753 (constructor NvidiaSubmissionByteShape NvidiaSubmissionByteShapeValue
754 (naturalAdd (nvidiaSubmissionPaddedBytesOf left) (nvidiaSubmissionPaddedBytesOf right))
755 (naturalSelect (naturalIsZero (nvidiaSubmissionPaddedBytesOf right))
756 (nvidiaSubmissionFinalPaddingOf left) (nvidiaSubmissionFinalPaddingOf right)))))
757def nvidiaSubmissionByteShapeRepeat = (lambda unrestricted count : Nat .
758 (lambda unrestricted shape : (family NvidiaSubmissionByteShape) .
759 (constructor NvidiaSubmissionByteShape NvidiaSubmissionByteShapeValue
760 (naturalMultiply count (nvidiaSubmissionPaddedBytesOf shape))
761 (naturalMultiply (naturalNonzero count) (nvidiaSubmissionFinalPaddingOf shape)))))
762def nvidiaSubmissionBatchShape = (lambda unrestricted profiled : Nat . (lambda unrestricted references : Nat .
763 (let unrestricted encoded = (naturalAdd (nvidiaSubmissionBatchBytes references)
764 (naturalMultiply (naturalNonzero profiled) (naturalMultiply references nvidiaSubmissionReleaseBytes))) in
765 (let unrestricted padded = (naturalMultiply nvidiaCodeRegionAlignment
766 (naturalDivideUnchecked (naturalAdd encoded (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1)) nvidiaCodeRegionAlignment)) in
767 (constructor NvidiaSubmissionByteShape NvidiaSubmissionByteShapeValue padded
768 (naturalSaturatingSubtract padded encoded))))))
769
770def nvidiaSubmissionScheduleByteShape = (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
771 (eliminate NvidiaSubmissionSchedule
772 (lambda unrestricted current : (family NvidiaSubmissionSchedule) .
773 (pi unrestricted profiled : Nat . (family NvidiaSubmissionByteShape)))
774 schedule
775 (branch NvidiaSubmissionScheduleEmpty . (lambda unrestricted profiled : Nat .
776 (constructor NvidiaSubmissionByteShape NvidiaSubmissionByteShapeValue 0 0)))
777 (branch NvidiaSubmissionScheduleOne batch . (lambda unrestricted profiled : Nat .
778 (eliminate NvidiaSubmissionBatch (lambda unrestricted current : (family NvidiaSubmissionBatch) . (family NvidiaSubmissionByteShape))
779 batch (branch NvidiaSubmissionBatchValue identity offset references .
780 (nvidiaSubmissionBatchShape profiled (nvidiaLaunchReferencesCount references))))))
781 (branch NvidiaSubmissionScheduleAppend left right leftShape rightShape . (lambda unrestricted profiled : Nat .
782 (nvidiaSubmissionByteShapeAppend (leftShape profiled) (rightShape profiled))))
783 (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyShape . (lambda unrestricted profiled : Nat .
784 (nvidiaSubmissionByteShapeRepeat count (bodyShape profiled))))
785 (branch NvidiaSubmissionScheduleProfiled offset body bodyShape . (lambda unrestricted profiled : Nat .
786 (bodyShape 1)))))
787
788-- This is an extent calculation, not plan admission. Invalid or empty launch
789-- reference sets still have to be refused by the whole-program encoder.
790def nvidiaSubmissionScheduleEncodedBytes = (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) .
791 (let unrestricted shape = (nvidiaSubmissionScheduleByteShape schedule 0) in
792 (naturalSaturatingSubtract (nvidiaSubmissionPaddedBytesOf shape) (nvidiaSubmissionFinalPaddingOf shape))))
793
794
795def nvidiaLaunchScheduleCount =
796 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
797 (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule
798 (branch NvidiaLaunchScheduleEmpty . 0)
799 (branch NvidiaLaunchScheduleOne launch . 1)
800 (branch NvidiaLaunchScheduleAppend left right leftCount rightCount . (naturalAdd leftCount rightCount))
801 (branch NvidiaLaunchScheduleRepeat count iteration body bodyCount . (naturalMultiply count bodyCount))))
802
803-- Constant blocks have per-launch alignment. Derive their storage from the
804-- same schedule that supplies the launches, so a changed phase cannot leave
805-- an independently maintained count or byte capacity behind.
806def nvidiaLaunchParameterBytes =
807 (lambda unrestricted alignment : Nat . (lambda unrestricted launch : (family NvidiaLaunchTemplate) .
808 (eliminate NvidiaLaunchTemplate (lambda unrestricted current : (family NvidiaLaunchTemplate) . Nat) launch
809 (branch NvidiaLaunchTemplateValue name kernel parameters .
810 (eliminate NvidiaLaunchKernel (lambda unrestricted current : (family NvidiaLaunchKernel) . Nat) kernel
811 (branch NvidiaLaunchKernelValue program x y z by bz bytes .
812 (naturalMultiply alignment
813 (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract alignment 1)) alignment))))))))
814def nvidiaLaunchScheduleParameterBytes =
815 (lambda unrestricted alignment : Nat . (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
816 (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule
817 (branch NvidiaLaunchScheduleEmpty . 0)
818 (branch NvidiaLaunchScheduleOne launch . (nvidiaLaunchParameterBytes alignment launch))
819 (branch NvidiaLaunchScheduleAppend left right leftBytes rightBytes . (naturalAdd leftBytes rightBytes))
820 (branch NvidiaLaunchScheduleRepeat count iteration body bodyBytes . (naturalMultiply count bodyBytes)))))
821
822-- Reserve exact per-launch constant extents after all canonical images.
823-- The backend may prune images but cannot require more code or parameter
824-- storage than this bound. Both terms come from the typed inputs it encodes.
825def nvidiaSM86ProgramCapacity =
826 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
827 (lambda unrestricted launches : (family NvidiaLaunchSchedule) .
828 (naturalAdd
829 (nvidiaCodeRegionExtent (nvidiaSM86RegionsPlacedEnd regions))
830 (nvidiaLaunchScheduleParameterBytes
831 nvidiaCodeRegionAlignment launches))))
832
833def nvidiaSM86ScalarRegion =
834 (lambda unrestricted identity : Bytes .
835 (lambda unrestricted program : (family SM86Program) .
836 (lambda unrestricted unavailable : Bytes .
837 (constructor
838 NvidiaDeviceRegion
839 NvidiaDeviceProgramRegion
840 identity
841 program
842 (sm86RegisterDemand program)
843 1
844 0
845 (constructor NvidiaDeviceRealization NvidiaDeviceRealizationRefused unavailable)))))
846
847-- Scalar pointer ABI shared by state programs and arithmetic regions. The
848-- target compiler owns region placement, pointer fields and constant extent.
849def nvidiaSM86PointerKernelLaunch =
850 (lambda unrestricted identity : Bytes .
851 (lambda unrestricted regions : (family NvidiaDeviceRegions) .
852 (lambda unrestricted programBase : Nat .
853 (lambda unrestricted pointers : (family StdList Nat) .
854 (constructor
855 NvidiaLaunchTemplate
856 NvidiaLaunchTemplateValue
857 identity
858 (constructor
859 NvidiaLaunchKernel
860 NvidiaLaunchKernelValue
861 -- The source label does not select code. Name the canonical
862 -- region placement; the whole-program compiler then retains
863 -- and relocates that region with its own register requirements.
864 (modelWord64FromNaturalTruncated
865 (naturalAdd programBase (nvidiaSM86RegionOffsetFrom identity regions 0)))
866 1
867 1
868 1
869 1
870 1
871 (nvidiaKernelConstantExtent
872 (nvidiaKernelPointerByteOffset (stdListLength Nat pointers))))
873 (nvidiaParameterBlockFromList
874 (app
875 (eliminate
876 StdList
877 (lambda unrestricted values : (family StdList Nat) .
878 (pi unrestricted index : Nat . (family StdList (family NvidiaParameterPatch))))
879 pointers
880 (branch
881 StdListEmpty
882 .
883 (lambda unrestricted index : Nat .
884 (constructor StdList StdListEmpty (family NvidiaParameterPatch))))
885 (branch
886 StdListCons
887 address
888 tail
889 rest
890 .
891 (lambda unrestricted index : Nat .
892 (constructor
893 StdList
894 StdListCons
895 (family NvidiaParameterPatch)
896 (nvidiaKernelPointerPatch index address)
897 (rest (succ index))))))
898 0)))))))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.