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