module Hardware.Nvidia.SM86.Command.WholeProgramPlan import Accelerator.SM86.Instruction import Accelerator.SM86.InstructionEncoding import Accelerator.SM86.Program import Hardware.Nvidia.SM86.Command.QMD import Std.Natural import Std.Foundation import Std.List import Data.Bytes import Model.Config import Model.Parameter import Model.Word64 -- A program's machine code on a target that does not run its SM86 words -- (sm_121's: Accelerator.SM121.Lowering), or why it has none. family NvidiaDeviceRealization : Type 0 constructor NvidiaDeviceRealized field unrestricted nvidiaDeviceRealizedMaterial : Bytes constructor NvidiaDeviceRealizationRefused field unrestricted nvidiaDeviceRealizationRefusal : Bytes end-family -- Target-owned, typed inputs to late NVIDIA component realization. These -- values remain ordinary Alpha data until whole-program erasure has selected a -- concrete target. `compiler-native-encode` is the backend boundary: it -- lowers this public representation without making a model own wire layouts. family NvidiaDeviceRegion : Type 0 constructor NvidiaDeviceRegionValue field unrestricted nvidiaDeviceRegionIdentity : Bytes field unrestricted nvidiaDeviceRegionMaterial : Bytes field unrestricted nvidiaDeviceRegionRegisters : Nat field unrestricted nvidiaDeviceRegionBlockX : Nat field unrestricted nvidiaDeviceRegionSharedBytes : Nat -- SM121 needs an explicit barrier allocation. The older constructor cannot -- be silently reinterpreted as Blackwell: its resource contract lacks this -- field and its machine image belongs to another instruction profile. constructor NvidiaDeviceRegionSM121 field unrestricted nvidiaSM121RegionIdentity : Bytes field unrestricted nvidiaSM121RegionMaterial : Bytes field unrestricted nvidiaSM121RegionRegisters : Nat field unrestricted nvidiaSM121RegionBlockX : Nat field unrestricted nvidiaSM121RegionSharedBytes : Nat field unrestricted nvidiaSM121RegionBarrierCount : Nat -- A region given as its typed SM86 program: its canonical placement is the -- program's SM86 encoding, and the backend places the machine code of the -- plan's target: the SM86 words, or the sm_121 realization (read only for an -- sm_121 plan). constructor NvidiaDeviceProgramRegion field unrestricted nvidiaDeviceProgramRegionIdentity : Bytes field unrestricted nvidiaDeviceProgramRegionProgram : (family SM86Program) field unrestricted nvidiaDeviceProgramRegionRegisters : Nat field unrestricted nvidiaDeviceProgramRegionBlockX : Nat field unrestricted nvidiaDeviceProgramRegionSharedBytes : Nat field unrestricted nvidiaDeviceProgramRegionSM121 : (family NvidiaDeviceRealization) end-family family NvidiaDeviceRegions : Type 0 constructor NvidiaDeviceRegionsEnd constructor NvidiaDeviceRegionsNext field unrestricted nvidiaDeviceRegionsHead : (family NvidiaDeviceRegion) recursive unrestricted nvidiaDeviceRegionsTail end-family -- Kernel parameters remain typed sparse words until late realization. The -- backend supplies zero-filled storage, checks every word offset against the -- launch's declared constant extent, and chooses the final program or spill -- address only after device-region erasure and compaction. family NvidiaParameterPatch : Type 0 constructor NvidiaParameterPatchValue field unrestricted nvidiaParameterPatchWordOffset : Nat field unrestricted nvidiaParameterPatchWordValue : (family ModelWord64) end-family family NvidiaParameterPatches : Type 0 constructor NvidiaParameterPatchesEnd constructor NvidiaParameterPatchesNext field unrestricted nvidiaParameterPatchesHead : (family NvidiaParameterPatch) recursive unrestricted nvidiaParameterPatchesTail end-family family NvidiaParameterBlock : Type 0 constructor NvidiaParameterBlockValue field unrestricted nvidiaParameterBlockPatches : (family NvidiaParameterPatches) end-family -- Repeat adjustments name a block ordinal within the expanded repeated body, -- or every block when one training scalar is shared by a phase. Affine and -- quotient/remainder adjustments are deltas; table frames are exact values. family NvidiaParameterAdjustmentScope : Type 0 constructor NvidiaParameterAdjustmentAllBlocks constructor NvidiaParameterAdjustmentBlock field unrestricted nvidiaParameterAdjustmentBlockOrdinal : Nat end-family family NvidiaParameterAdjustment : Type 0 constructor NvidiaParameterAdjustmentValue field unrestricted nvidiaParameterAdjustmentScope : (family NvidiaParameterAdjustmentScope) field unrestricted nvidiaParameterAdjustmentWordOffset : Nat field unrestricted nvidiaParameterAdjustmentWordValue : (family ModelWord64) end-family family NvidiaParameterAdjustments : Type 0 constructor NvidiaParameterAdjustmentsEnd constructor NvidiaParameterAdjustmentsNext field unrestricted nvidiaParameterAdjustmentsHead : (family NvidiaParameterAdjustment) recursive unrestricted nvidiaParameterAdjustmentsTail end-family family NvidiaParameterAdjustmentFrames : Type 0 constructor NvidiaParameterAdjustmentFramesEnd constructor NvidiaParameterAdjustmentFramesNext field unrestricted nvidiaParameterAdjustmentFrame : (family NvidiaParameterAdjustments) recursive unrestricted nvidiaParameterAdjustmentFramesTail end-family family NvidiaParameterIteration : Type 0 constructor NvidiaParameterIterationUnchanged constructor NvidiaParameterIterationAffine field unrestricted nvidiaParameterIterationAffineDeltas : (family NvidiaParameterAdjustments) constructor NvidiaParameterIterationQuotientRemainder field unrestricted nvidiaParameterIterationDivisor : Nat field unrestricted nvidiaParameterIterationRemainderDeltas : (family NvidiaParameterAdjustments) field unrestricted nvidiaParameterIterationQuotientDeltas : (family NvidiaParameterAdjustments) constructor NvidiaParameterIterationTable field unrestricted nvidiaParameterIterationFrames : (family NvidiaParameterAdjustmentFrames) end-family -- A launch names a typed device region by its pre-compaction address and -- carries only semantic launch geometry and constant-buffer placement. Code -- extent, prefetch width, block X, register count and shared memory are -- deliberately absent: the backend derives those fields from the retained -- device region after whole-program erasure. family NvidiaLaunchKernel : Type 0 constructor NvidiaLaunchKernelValue field unrestricted nvidiaLaunchProgramAddress : (family ModelWord64) field unrestricted nvidiaLaunchGridX : Nat field unrestricted nvidiaLaunchGridY : Nat field unrestricted nvidiaLaunchGridZ : Nat field unrestricted nvidiaLaunchBlockY : Nat field unrestricted nvidiaLaunchBlockZ : Nat field unrestricted nvidiaLaunchConstantBytes : Nat end-family family NvidiaLaunchTemplate : Type 0 constructor NvidiaLaunchTemplateValue field unrestricted nvidiaLaunchSourceIdentity : Bytes field unrestricted nvidiaLaunchKernel : (family NvidiaLaunchKernel) field unrestricted nvidiaLaunchParameters : (family NvidiaParameterBlock) end-family -- Repeated training phases stay compact in source. Parameter iteration -- metadata transforms sparse words without duplicating parameter blocks, -- device images or descriptor bytes in the checked graph. family NvidiaLaunchSchedule : Type 0 constructor NvidiaLaunchScheduleEmpty constructor NvidiaLaunchScheduleOne field unrestricted nvidiaLaunchScheduleLaunch : (family NvidiaLaunchTemplate) constructor NvidiaLaunchScheduleAppend recursive unrestricted nvidiaLaunchScheduleLeft recursive unrestricted nvidiaLaunchScheduleRight constructor NvidiaLaunchScheduleRepeat field unrestricted nvidiaLaunchScheduleRepeatCount : Nat field unrestricted nvidiaLaunchScheduleParameterIteration : (family NvidiaParameterIteration) recursive unrestricted nvidiaLaunchScheduleRepeatedBody end-family -- Submission ranges refer to ordinals in the realized QMD table. Pushbuffer -- methods and GPFIFO entries are derived from these ranges after launch -- erasure; neither their addresses nor padding are frozen in model source. family NvidiaLaunchReferences : Type 0 constructor NvidiaLaunchReferencesEmpty constructor NvidiaLaunchReferencesRange field unrestricted nvidiaLaunchReferenceFirst : Nat field unrestricted nvidiaLaunchReferenceCount : Nat constructor NvidiaLaunchReferencesAppend recursive unrestricted nvidiaLaunchReferencesLeft recursive unrestricted nvidiaLaunchReferencesRight end-family family NvidiaSubmissionBatch : Type 0 constructor NvidiaSubmissionBatchValue field unrestricted nvidiaSubmissionSourceIdentity : Bytes field unrestricted nvidiaSubmissionSemaphoreOffset : Nat field unrestricted nvidiaSubmissionReferences : (family NvidiaLaunchReferences) end-family family NvidiaSubmissionSchedule : Type 0 constructor NvidiaSubmissionScheduleEmpty constructor NvidiaSubmissionScheduleOne field unrestricted nvidiaSubmissionScheduleBatch : (family NvidiaSubmissionBatch) constructor NvidiaSubmissionScheduleAppend recursive unrestricted nvidiaSubmissionScheduleLeft recursive unrestricted nvidiaSubmissionScheduleRight constructor NvidiaSubmissionScheduleRepeat field unrestricted nvidiaSubmissionScheduleRepeatCount : Nat field unrestricted nvidiaSubmissionReferenceStride : Nat field unrestricted nvidiaSubmissionSemaphoreStride : Nat recursive unrestricted nvidiaSubmissionScheduleRepeatedBody -- The same submissions, each launch followed by a semaphore release that -- waits for it to finish and carries the device's timestamp, at `offset` + -- 16 x the launch's QMD ordinal from the plan's semaphore base (its payload -- the ordinal): the device time of every launch, for a profile. Waiting for -- each launch serializes launches the plan would otherwise let overlap, so a -- profile's step is not the production step's time. constructor NvidiaSubmissionScheduleProfiled field unrestricted nvidiaSubmissionProfileOffset : Nat recursive unrestricted nvidiaSubmissionProfiledBody end-family family NvidiaQMDRecipeBlocks : Type 0 constructor NvidiaQMDRecipeBlocksEnd constructor NvidiaQMDRecipeBlocksNext field unrestricted nvidiaQMDRecipeBlockIdentity : Bytes field unrestricted nvidiaQMDRecipeBlockOutputBytes : (family ModelWord64) field unrestricted nvidiaQMDRecipeBlockRecordCount : Nat field unrestricted nvidiaQMDRecipeBlockZeroRecords : Nat field unrestricted nvidiaQMDRecipeBlockRecords : Bytes recursive unrestricted nvidiaQMDRecipeBlocksTail end-family family NvidiaPackbitsRecipeBlocks : Type 0 constructor NvidiaPackbitsRecipeBlocksEnd constructor NvidiaPackbitsRecipeBlocksNext field unrestricted nvidiaPackbitsRecipeBlockIdentity : Bytes field unrestricted nvidiaPackbitsRecipeBlockOutputBytes : (family ModelWord64) field unrestricted nvidiaPackbitsRecipeBlockCommandCount : Nat field unrestricted nvidiaPackbitsRecipeBlockBytes : Bytes recursive unrestricted nvidiaPackbitsRecipeBlocksTail end-family family NvidiaPushRecipeBlocks : Type 0 constructor NvidiaPushRecipeBlocksEnd constructor NvidiaPushRecipeBlocksNext field unrestricted nvidiaPushRecipeBlockPushIdentity : Bytes field unrestricted nvidiaPushRecipeBlockPushBytes : (family ModelWord64) field unrestricted nvidiaPushRecipeBlockGPFIFOIdentity : Bytes field unrestricted nvidiaPushRecipeBlockGPFIFOBytes : (family ModelWord64) field unrestricted nvidiaPushRecipeBlockBatchCount : Nat field unrestricted nvidiaPushRecipeBlockBatches : Bytes recursive unrestricted nvidiaPushRecipeBlocksTail end-family family NvidiaPhysicalComponentPlan : Type 0 constructor NvidiaProgramComponentPlan field unrestricted nvidiaProgramImages : Bytes field unrestricted nvidiaProgramImageCursor : Nat field unrestricted nvidiaProgramImageCount : Nat field unrestricted nvidiaProgramExpectedImageCursor : Nat field unrestricted nvidiaProgramExpectedImageCount : Nat field unrestricted nvidiaProgramGapBytes : Nat field unrestricted nvidiaProgramRecipeCommands : Nat field unrestricted nvidiaProgramRecipe : Bytes field unrestricted nvidiaProgramRecipeDropBytes : Nat field unrestricted nvidiaProgramOutputBytes : Nat constructor NvidiaQMDComponentPlan field unrestricted nvidiaQMDArchitecture : (family ModelWord32) field unrestricted nvidiaQMDBlocks : (family NvidiaQMDRecipeBlocks) constructor NvidiaPackbitsComponentPlan field unrestricted nvidiaPackbitsPrefixZeroBytes : Nat field unrestricted nvidiaPackbitsBlocks : (family NvidiaPackbitsRecipeBlocks) constructor NvidiaPushComponentPlan field unrestricted nvidiaPushComputeClass : (family ModelWord32) field unrestricted nvidiaPushSPAVersion : (family ModelWord32) field unrestricted nvidiaPushBlocks : (family NvidiaPushRecipeBlocks) constructor NvidiaGPFIFOComponentPlan field unrestricted nvidiaGPFIFOComputeClass : (family ModelWord32) field unrestricted nvidiaGPFIFOSPAVersion : (family ModelWord32) field unrestricted nvidiaGPFIFOBlocks : (family NvidiaPushRecipeBlocks) end-family -- One connected late-realization plan. Program compaction and QMD rewriting -- consume this value together, so a descriptor cannot retain an address or a -- resource count from an erased or superseded device region. The historical -- recipe parameter offset and component capacity are compatibility bounds for -- the current host protocol, not output-layout requirements: retained images -- are repacked and their QMD fields are derived again before the component is -- padded to the admitted arena capacity. family NvidiaWholeProgramComponent : Type 0 constructor NvidiaWholeProgramProgram constructor NvidiaWholeProgramQMD constructor NvidiaWholeProgramPushbuffer constructor NvidiaWholeProgramGPFIFO -- The same four tables as launch-table recipes: the compact form the host -- expands into the mapped arena at startup with the shared -- Runtime.NativeLaunchRecipeRoutine. The compiler derives each recipe from -- the schedule's repeat structure and publishes it only after it has expanded -- it back to the exact table bytes. constructor NvidiaWholeProgramProgramRecipe constructor NvidiaWholeProgramQMDRecipe constructor NvidiaWholeProgramPushbufferRecipe constructor NvidiaWholeProgramGPFIFORecipe -- The device address of each launch's parameter block, in launch order (a -- little-endian u64 each), as the realization placed it: in the program -- region after the retained code, or past the QMD table. A host that -- supplies a parameter word at run time writes it there. constructor NvidiaWholeProgramParameterAddresses -- The 8-byte word at a byte offset of each launch's parameter block, in -- launch order, as realized (0 past the block's extent): what a host that -- supplies a word at run time checks its sites against. constructor NvidiaWholeProgramParameterWords field unrestricted nvidiaWholeProgramParameterWordOffset : Nat -- The launch manifest, one text line per launch in QMD order: the ordinal, -- the launch's source identity and its device region's identity, separated -- by tabs. A per-launch profile (NvidiaSubmissionScheduleProfiled) records -- one stamp per QMD ordinal; the manifest names what each ordinal ran. constructor NvidiaWholeProgramLaunchIdentities end-family family NvidiaWholeProgramPlan : Type 0 constructor NvidiaWholeProgramPlanValue field unrestricted nvidiaWholeProgramComponent : (family NvidiaWholeProgramComponent) field unrestricted nvidiaWholeProgramArchitecture : (family ModelWord32) field unrestricted nvidiaWholeProgramComputeClass : (family ModelWord32) field unrestricted nvidiaWholeProgramSPAVersion : (family ModelWord32) field unrestricted nvidiaWholeProgramProgramBase : (family ModelWord64) field unrestricted nvidiaWholeProgramQMDBase : (family ModelWord64) field unrestricted nvidiaWholeProgramPushbufferBase : (family ModelWord64) field unrestricted nvidiaWholeProgramSemaphoreBase : (family ModelWord64) field unrestricted nvidiaWholeProgramRegionAlignment : Nat field unrestricted nvidiaWholeProgramProgramCapacity : Nat field unrestricted nvidiaWholeProgramRegions : (family NvidiaDeviceRegions) field unrestricted nvidiaWholeProgramLaunchSchedule : (family NvidiaLaunchSchedule) field unrestricted nvidiaWholeProgramExpectedLaunchCount : Nat field unrestricted nvidiaWholeProgramQMDTableBytes : Nat field unrestricted nvidiaWholeProgramSubmissions : (family NvidiaSubmissionSchedule) field unrestricted nvidiaWholeProgramExpectedSubmissionCount : Nat field unrestricted nvidiaWholeProgramExpectedReferenceCount : Nat end-family def nvidiaLaunchFirstOrdinal : Nat = 0 def nvidiaSubmissionFirstSemaphoreOffset : Nat = 0 def nvidiaLaunchReferencesCount = (lambda unrestricted references : (family NvidiaLaunchReferences) . (eliminate NvidiaLaunchReferences (lambda unrestricted current : (family NvidiaLaunchReferences) . Nat) references (branch NvidiaLaunchReferencesEmpty . 0) (branch NvidiaLaunchReferencesRange first count . count) (branch NvidiaLaunchReferencesAppend left right leftCount rightCount . (naturalAdd leftCount rightCount)))) def nvidiaSubmissionScheduleCount = (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) . (eliminate NvidiaSubmissionSchedule (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat) schedule (branch NvidiaSubmissionScheduleEmpty . 0) (branch NvidiaSubmissionScheduleOne batch . 1) (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount . (naturalAdd leftCount rightCount)) (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount . (naturalMultiply count bodyCount)) (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount))) def nvidiaSubmissionScheduleReferenceCount = (lambda unrestricted schedule : (family NvidiaSubmissionSchedule) . (eliminate NvidiaSubmissionSchedule (lambda unrestricted current : (family NvidiaSubmissionSchedule) . Nat) schedule (branch NvidiaSubmissionScheduleEmpty . 0) (branch NvidiaSubmissionScheduleOne batch . (eliminate NvidiaSubmissionBatch (lambda unrestricted current : (family NvidiaSubmissionBatch) . Nat) batch (branch NvidiaSubmissionBatchValue identity semaphore references . (nvidiaLaunchReferencesCount references)))) (branch NvidiaSubmissionScheduleAppend left right leftCount rightCount . (naturalAdd leftCount rightCount)) (branch NvidiaSubmissionScheduleRepeat count referenceStride semaphoreStride body bodyCount . (naturalMultiply count bodyCount)) (branch NvidiaSubmissionScheduleProfiled offset body bodyCount . bodyCount))) -- A launch can declare ordered, typed patches without nesting one constructor -- per ABI argument. Validation of offsets and extent still belongs to the -- late parameter-block realization, after image pruning and placement. def nvidiaParameterPatchesFromList = (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) . (eliminate StdList (lambda unrestricted current : (family StdList (family NvidiaParameterPatch)) . (family NvidiaParameterPatches)) patches (branch StdListEmpty . (constructor NvidiaParameterPatches NvidiaParameterPatchesEnd)) (branch StdListCons head tail induction . (constructor NvidiaParameterPatches NvidiaParameterPatchesNext head induction)))) def nvidiaParameterBlockFromList = (lambda unrestricted patches : (family StdList (family NvidiaParameterPatch)) . (constructor NvidiaParameterBlock NvidiaParameterBlockValue (nvidiaParameterPatchesFromList patches))) -- A layer may reuse the same typed image and launch geometry while its -- parameter pointers change. Keeping identity and kernel together prevents -- callers from restating hardware launch facts for each layer. def nvidiaLaunchWithParameters = (lambda unrestricted launch : (family NvidiaLaunchTemplate) . (lambda unrestricted parameters : (family NvidiaParameterBlock) . (eliminate NvidiaLaunchTemplate (lambda unrestricted current : (family NvidiaLaunchTemplate) . (family NvidiaLaunchTemplate)) launch (branch NvidiaLaunchTemplateValue identity kernel previous . (constructor NvidiaLaunchTemplate NvidiaLaunchTemplateValue identity kernel parameters))))) def nvidiaLaunchSequence = (lambda unrestricted launches : (family StdList (family NvidiaLaunchTemplate)) . (stdListFold (family NvidiaLaunchTemplate) (family NvidiaLaunchSchedule) (lambda unrestricted launch : (family NvidiaLaunchTemplate) . (lambda unrestricted tail : (family NvidiaLaunchSchedule) . (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleAppend (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleOne launch) tail))) (constructor NvidiaLaunchSchedule NvidiaLaunchScheduleEmpty) launches)) -- CB0 uses 64-bit pointer slots after the target QMD parameter header. -- Systems supply addresses from their arena layout, not literal word slots. def nvidiaKernelBlockXWord : Nat = (naturalDivideUnchecked qmdBlockDimensionXOffset 8) def nvidiaKernelPointerSlotBytes : Nat = 8 def nvidiaKernelPointerByteOffset = (lambda unrestricted argument : Nat . (naturalAdd qmdKernelParameterBase (naturalMultiply nvidiaKernelPointerSlotBytes argument))) def nvidiaKernelPointerWord = (lambda unrestricted argument : Nat . (naturalDivideUnchecked (nvidiaKernelPointerByteOffset argument) nvidiaKernelPointerSlotBytes)) def nvidiaKernelPointerPatch = (lambda unrestricted argument : Nat . (lambda unrestricted address : Nat . (constructor NvidiaParameterPatch NvidiaParameterPatchValue (nvidiaKernelPointerWord argument) (modelWord64FromNaturalTruncated address)))) def nvidiaKernelU32WordPatch = (lambda unrestricted slot : Nat . (lambda unrestricted word : Nat . (lambda erased admitted : (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) . (constructor NvidiaParameterPatch NvidiaParameterPatchValue slot (modelWord64FromNaturalTruncated word))))) -- Two neighboring 32-bit CB0 scalars share one 64-bit sparse patch. Packing -- them here prevents a later patch from overwriting the first scalar. def nvidiaKernelU32PairPatch = (lambda unrestricted argument : Nat . (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . (lambda erased lowAdmitted : (equal Nat (naturalLess low (naturalPowerOfTwo 32)) 1) . (lambda erased highAdmitted : (equal Nat (naturalLess high (naturalPowerOfTwo 32)) 1) . (constructor NvidiaParameterPatch NvidiaParameterPatchValue (nvidiaKernelPointerWord argument) (modelWord64FromNaturalTruncated (naturalAdd low (naturalMultiply high (naturalPowerOfTwo 32)))))))))) -- A whole-table certificate admits dynamic indices whose selected values -- cannot be reduced while checking a launch-construction lambda. An index -- beyond the list yields zero; the schedule owner separately proves length. def nvidiaKernelU32TableOverflowCount = (lambda unrestricted table : (family StdList Nat) . (stdListFold Nat Nat (lambda unrestricted word : Nat . (lambda unrestricted count : Nat . (naturalAdd count (naturalSelect (naturalLess word (naturalPowerOfTwo 32)) 0 1)))) 0 table)) def nvidiaKernelU32TableWordAt = (lambda unrestricted table : (family StdList Nat) . (lambda unrestricted index : Nat . (stdOptionValueOr Nat 0 (stdListIndex Nat table index)))) def nvidiaKernelU32PairPatchFromCertifiedTable = (lambda unrestricted argument : Nat . (lambda unrestricted table : (family StdList Nat) . (lambda unrestricted index : Nat . (lambda erased admitted : (equal Nat (nvidiaKernelU32TableOverflowCount table) 0) . (constructor NvidiaParameterPatch NvidiaParameterPatchValue (nvidiaKernelPointerWord argument) (modelWord64FromNaturalTruncated (naturalAdd (nvidiaKernelU32TableWordAt table index) (naturalMultiply (nvidiaKernelU32TableWordAt table (succ index)) (naturalPowerOfTwo 32))))))))) def nvidiaKernelF32ScalarPatch = (lambda unrestricted argument : Nat . (lambda unrestricted word : Nat . (lambda erased admitted : (equal Nat (naturalLess word (naturalPowerOfTwo 32)) 1) . (nvidiaKernelU32WordPatch (nvidiaKernelPointerWord argument) word admitted)))) -- Compose independently owned device closures before whole-program pruning. -- This preserves order; placement and duplicate-identity admission remain -- the whole-program planner's responsibility. def nvidiaAppendDeviceRegions = (lambda unrestricted left : (family NvidiaDeviceRegions) . (lambda unrestricted right : (family NvidiaDeviceRegions) . (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . (family NvidiaDeviceRegions)) left (branch NvidiaDeviceRegionsEnd . right) (branch NvidiaDeviceRegionsNext head tail induction . (constructor NvidiaDeviceRegions NvidiaDeviceRegionsNext head induction))))) -- how many launches a schedule expands to -- Extents of the v1 submission protocol used by the backend: initialization -- has four two-word methods, three three-word methods, and 64 two-word CWD -- counter methods. Each of the two semaphore releases is six words; a launch -- is three two-word methods. Keep sizing separate from byte encoding so a -- placement proof need not normalize a machine image. Artifact gates compare -- this extent with the backend's actual output before accepting the image. def nvidiaCodeRegionAlignment : Nat = 256 def nvidiaCodeRegionExtent = (lambda unrestricted bytes : Nat . (naturalMultiply nvidiaCodeRegionAlignment (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1)) nvidiaCodeRegionAlignment))) -- SM86 placement uses the same 256-byte alignment and 16-byte instruction -- extent as nativePlaceNvidiaRegions. A target-specific lookup is required: -- SM121 lowering can change a typed program's byte extent. def nvidiaSM86RegionIdentity = (lambda unrestricted region : (family NvidiaDeviceRegion) . (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Bytes) region (branch NvidiaDeviceRegionValue identity material registers block shared . identity) (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . identity) (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget . identity))) def nvidiaSM86RegionExtent = (lambda unrestricted region : (family NvidiaDeviceRegion) . (eliminate NvidiaDeviceRegion (lambda unrestricted current : (family NvidiaDeviceRegion) . Nat) region (branch NvidiaDeviceRegionValue identity material registers block shared . (bytes-length material)) (branch NvidiaDeviceRegionSM121 identity material registers block shared barriers . 0) (branch NvidiaDeviceProgramRegion identity program registers block shared otherTarget . (naturalMultiply sm86InstructionBytes (sm86ProgramCount program))))) def nvidiaSM86RegionsAdmitted = (lambda unrestricted regions : (family NvidiaDeviceRegions) . (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions (branch NvidiaDeviceRegionsEnd . 1) (branch NvidiaDeviceRegionsNext head tail induction . (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head)) induction)))) -- The end of the canonical region placement, before reachability pruning. -- A program arena sized from this upper bound remains valid when a launch -- disappears or code is compacted; each region starts at the same alignment -- nativePlaceNvidiaRegions uses for SM86. def nvidiaSM86RegionsPlacedEnd = (lambda unrestricted regions : (family NvidiaDeviceRegions) . (app (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . (pi unrestricted cursor : Nat . Nat)) regions (branch NvidiaDeviceRegionsEnd . (lambda unrestricted cursor : Nat . cursor)) (branch NvidiaDeviceRegionsNext head tail induction . (lambda unrestricted cursor : Nat . (induction (naturalAdd (nvidiaCodeRegionExtent cursor) (nvidiaSM86RegionExtent head)))))) 0)) def nvidiaSM86RegionPrefixAdmitted = (lambda unrestricted identity : Bytes . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . Nat) regions (branch NvidiaDeviceRegionsEnd . 0) (branch NvidiaDeviceRegionsNext head tail induction . (naturalAnd (naturalNonzero (nvidiaSM86RegionExtent head)) (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity) 1 induction)))))) def nvidiaSM86RegionOffsetFrom = (lambda unrestricted identity : Bytes . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (eliminate NvidiaDeviceRegions (lambda unrestricted current : (family NvidiaDeviceRegions) . (pi unrestricted cursor : Nat . Nat)) regions (branch NvidiaDeviceRegionsEnd . (lambda unrestricted cursor : Nat . 0)) (branch NvidiaDeviceRegionsNext head tail induction . (lambda unrestricted cursor : Nat . (let unrestricted placed = (nvidiaCodeRegionExtent cursor) in (naturalSelect (bytes-equal (nvidiaSM86RegionIdentity head) identity) placed (induction (naturalAdd placed (nvidiaSM86RegionExtent head)))))))))) def nvidiaSM86RegionAddressAdmitted = (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (naturalAnd (naturalNonzero base) (naturalAnd (naturalIsZero (naturalModuloUnchecked base nvidiaCodeRegionAlignment)) (nvidiaSM86RegionPrefixAdmitted identity regions)))))) def nvidiaSM86RegionAddress = (lambda unrestricted base : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted regions : (family NvidiaDeviceRegions) . (lambda erased admitted : (equal Nat (nvidiaSM86RegionAddressAdmitted base identity regions) 1) . (naturalAdd base (nvidiaSM86RegionOffsetFrom identity regions 0)))))) -- CB0 extents are rounded to QMD's sixteen-byte size unit, independently -- of the stronger alignment imposed on the parameter block's device VA. def nvidiaKernelConstantExtentUnit : Nat = 16 def nvidiaKernelConstantExtent = (lambda unrestricted argumentEnd : Nat . (naturalMultiply nvidiaKernelConstantExtentUnit (naturalDivideUnchecked (naturalAdd argumentEnd (naturalSaturatingSubtract nvidiaKernelConstantExtentUnit 1)) nvidiaKernelConstantExtentUnit))) def nvidiaSM121ConstantExtentUnit : Nat = nvidiaKernelConstantExtentUnit def nvidiaSM121ConstantExtent = nvidiaKernelConstantExtent def nvidiaSM121QMDRecordBytes : Nat = (naturalMultiply 96 4) def nvidiaSM121QMDSlotBytes : Nat = (naturalMultiply nvidiaCodeRegionAlignment (naturalDivideUnchecked (naturalAdd nvidiaSM121QMDRecordBytes (naturalSaturatingSubtract nvidiaCodeRegionAlignment 1)) nvidiaCodeRegionAlignment)) def nvidiaSubmissionWordBytes : Nat = 4 def nvidiaSubmissionBatchBytes = (lambda unrestricted launches : Nat . (naturalMultiply nvidiaSubmissionWordBytes (naturalAdd (naturalAdd (naturalMultiply 2 (naturalAdd 4 64)) (naturalMultiply 3 3)) (naturalAdd (naturalMultiply 2 6) (naturalMultiply launches (naturalMultiply 3 2)))))) -- A Blackwell batch is encoded as an Ampere one (the backend's -- nativeEncodeNvidiaSubmissionPieces, one target abstraction since the -- 2026-09-26 merge): the compute initialization with the target's class, -- SPA version and windows, the pre-launch release, per launch the PCAS -- address, schedule and shader-cache invalidation (6 words), the final -- release -- the encoding the Coppelius GB10 runs execute. The compiler -- checks actual recipe lengths. def nvidiaSM121SubmissionBatchBytes = nvidiaSubmissionBatchBytes -- A batch of `launches` launches followed by another, as the backend places -- it: carrying its padding to the next 256-byte boundary -- (nativeEncodeNvidiaSubmissionPieces); the last batch has none. def nvidiaPaddedSubmissionBatchBytes = (lambda unrestricted launches : Nat . (naturalMultiply (naturalDivideUnchecked (naturalAdd (nvidiaSubmissionBatchBytes launches) 255) 256) 256)) -- `count` batches of `launches` launches each def nvidiaUniformSubmissionBatchesBytes = (lambda unrestricted count : Nat . (lambda unrestricted launches : Nat . (naturalAdd (naturalMultiply (naturalSaturatingSubtract count 1) (nvidiaPaddedSubmissionBatchBytes launches)) (naturalSelect (naturalIsZero count) 0 (nvidiaSubmissionBatchBytes launches))))) def nvidiaLaunchScheduleCount = (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule (branch NvidiaLaunchScheduleEmpty . 0) (branch NvidiaLaunchScheduleOne launch . 1) (branch NvidiaLaunchScheduleAppend left right leftCount rightCount . (naturalAdd leftCount rightCount)) (branch NvidiaLaunchScheduleRepeat count iteration body bodyCount . (naturalMultiply count bodyCount)))) -- Constant blocks have per-launch alignment. Derive their storage from the -- same schedule that supplies the launches, so a changed phase cannot leave -- an independently maintained count or byte capacity behind. def nvidiaLaunchParameterBytes = (lambda unrestricted alignment : Nat . (lambda unrestricted launch : (family NvidiaLaunchTemplate) . (eliminate NvidiaLaunchTemplate (lambda unrestricted current : (family NvidiaLaunchTemplate) . Nat) launch (branch NvidiaLaunchTemplateValue name kernel parameters . (eliminate NvidiaLaunchKernel (lambda unrestricted current : (family NvidiaLaunchKernel) . Nat) kernel (branch NvidiaLaunchKernelValue program x y z by bz bytes . (naturalMultiply alignment (naturalDivideUnchecked (naturalAdd bytes (naturalSaturatingSubtract alignment 1)) alignment)))))))) def nvidiaLaunchScheduleParameterBytes = (lambda unrestricted alignment : Nat . (lambda unrestricted schedule : (family NvidiaLaunchSchedule) . (eliminate NvidiaLaunchSchedule (lambda unrestricted current : (family NvidiaLaunchSchedule) . Nat) schedule (branch NvidiaLaunchScheduleEmpty . 0) (branch NvidiaLaunchScheduleOne launch . (nvidiaLaunchParameterBytes alignment launch)) (branch NvidiaLaunchScheduleAppend left right leftBytes rightBytes . (naturalAdd leftBytes rightBytes)) (branch NvidiaLaunchScheduleRepeat count iteration body bodyBytes . (naturalMultiply count bodyBytes))))) -- Reserve exact per-launch constant extents after all canonical images. -- The backend may prune images but cannot require more code or parameter -- storage than this bound. Both terms come from the typed inputs it encodes. def nvidiaSM86ProgramCapacity = (lambda unrestricted regions : (family NvidiaDeviceRegions) . (lambda unrestricted launches : (family NvidiaLaunchSchedule) . (naturalAdd (nvidiaCodeRegionExtent (nvidiaSM86RegionsPlacedEnd regions)) (nvidiaLaunchScheduleParameterBytes nvidiaCodeRegionAlignment launches))))