module Platform.Linux.Nvidia.PlanHost import Data.Bytes import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Runtime.ArenaCertificate import Runtime.NativeLaunchRecipeLoad import Runtime.NativeTelemetry import Runtime.NativeTelemetrySeal import Runtime.NativePhysicalProgram import Runtime.NativePhysicalNativeELF import Runtime.NativePhysicalTrainingRoutine import Std.Natural -- The host the compiler derives from a whole-program plan: the compute-channel -- protocol the SM86 launch ladder proved on the RTX 3070 and the RTX 3090 -- (rungs D..Q, Coppelius S5, the checked linear step), as typed command -- builders parameterised by the plan's placement. Every address, extent and -- handle is a parameter or derived from one; the protocol is stated once, -- here, for every plan. -- -- Two lifecycles, selected by the layout: -- direct-RM every buffer is system memory; its GPU range is a fixed RM -- virtual reservation and a DMA map; the channel has 0x400 -- entries and its own USERD buffer. -- UVM RM's VA space is duplicated into the UVM driver; buffers are -- external ranges mapped through it; video-memory buffers are -- allowed and are not host-mapped; the GPFIFO is one contiguous -- video allocation whose last page is USERD; the channel is -- registered with UVM and scheduled last. This is the -- lifecycle the Coppelius training executables run. -- -- In order: open the card and the control node; root, device, subdevice, -- UVM: the DMA selector, the VA space, UVM: initialise the driver, register -- the GPU and the VA space, reserve the external range; the fixed buffers -- GPFIFO, pushbuffer, semaphores, program, QMD, direct-RM: USERD, and every -- data buffer; the error notifier; channel group, context share, channel, -- compute and usermode objects; direct-RM: bind, schedule, token, doorbell; -- UVM: doorbell, preemption, token, register the channel, schedule. Then -- the uploads, gpPut, the doorbell, a FenceWait on the plan's semaphore, the -- readbacks to stdout, exit 0. Every driver status is pre-set to a sentinel -- and recorded after the call; under NvidiaPlanHostStrict (the executables) -- each is asserted zero too, so a host without a card stops at its first -- device call with a command failure; under NvidiaPlanHostProbe (the -- channel probe) none after the root's is, and the host prints the status -- area. The root client is freed before exit. -- -- Measured on the RTX 3090, driver 580.126.09, 2026-09-22, the checked -- linear step: UVM lifecycle 11/11 runs; two submissions per host, one -- semaphore slot each: 6/6, both slots released with timestamps. The -- direct-RM channel allocation used to fail NV_ERR_INSUFFICIENT_RESOURCES -- 0x1e intermittently, in streaks, at a rate that drifted with the host -- machine's other tenants (3/10 .. 17/60). Root-caused 2026-09-23 with the -- channel probe, one placement at a time interleaved with the baseline: -- the cause is USERD as a separate SYSTEM-memory allocation. Not the -- channel flags, the bind, the schedule, the root free, the work, the -- GPFIFO's memory or the error notifier's (each within noise of the -- baseline); USERD in video memory 0/60 against 17/60, and the step with -- USERD in video memory 60/60 records bit-identical against 6/60 failures -- of the old host interleaved. The Ampere direct-RM profile therefore admits -- a layout only with a video-memory USERD (nvidiaPlanHostLayoutAdmitted); -- the UVM lifecycle's USERD is the last page of its video GPFIFO already. -- System memory is one physically contiguous allocation; paged system -- memory is not (NVOS32 PHYSICALITY NONCONTIGUOUS), which is what a buffer -- too large for contiguous pages needs -- the GB10's arena, which has no -- video memory to live in. The GPU reaches either through its page tables. family NvidiaPlanHostMemory : Type 0 constructor NvidiaPlanHostSystemMemory constructor NvidiaPlanHostVideoMemory -- Noncontiguous physical pages, still host-cached and GPU virtually contiguous. constructor NvidiaPlanHostPagedSystemMemory -- Noncontiguous system memory the GPU caches in its L2, in 64 KiB pages, -- never mapped into the process: the allocation cudaMalloc makes on the GB10 -- (read off the driver's RM calls, 2026-09-26: NV01_MEMORY_SYSTEM, attr -- PAGE_SIZE_BIG | LOCATION_PCI | PHYSICALITY_NONCONTIGUOUS, attr2 -- GPU_CACHEABLE_YES | ZBC_PREFER_NO_ZBC, flags IGNORE_BANK_PLACEMENT | -- MEMORY_HANDLE_PROVIDED | MAP_NOT_REQUIRED, PTE kind 6, 64 KiB aligned). -- Paged system memory is not L2-cached by the GPU: an L2-resident copy runs -- at 190 GB/s there against 880 GB/s here. constructor NvidiaPlanHostGPUCachedSystemMemory end-family -- host 0 = not mapped into the process family NvidiaPlanHostBuffer : Type 0 constructor NvidiaPlanHostBufferValue field unrestricted nvidiaPlanHostBufferIdentity : Bytes field unrestricted nvidiaPlanHostBufferGPU : Nat field unrestricted nvidiaPlanHostBufferHost : Nat field unrestricted nvidiaPlanHostBufferExtent : Nat field unrestricted nvidiaPlanHostBufferMemory : (family NvidiaPlanHostMemory) end-family family NvidiaPlanHostBuffers : Type 0 constructor NvidiaPlanHostBuffersEnd constructor NvidiaPlanHostBuffersNext field unrestricted nvidiaPlanHostBuffersHead : (family NvidiaPlanHostBuffer) recursive unrestricted nvidiaPlanHostBuffersTail end-family family NvidiaPlanHostABI : Type 0 constructor NvidiaPlanHostABIValue field unrestricted nvidiaPlanHostMapDMAIoctl : Nat field unrestricted nvidiaPlanHostNVOS46Size : Nat field unrestricted nvidiaPlanHostNVOS46DMAOffset : Nat field unrestricted nvidiaPlanHostNVOS46Status : Nat field unrestricted nvidiaPlanHostChannelClass : Nat field unrestricted nvidiaPlanHostComputeClass : Nat field unrestricted nvidiaPlanHostUsermodeClass : Nat field unrestricted nvidiaPlanHostEngineType : Nat -- the first four bytes of the driver version the ABI was built for, -- little-endian ("580." is 0x2E303835): the host asks the driver for its -- version before any card call and refuses another branch by name field unrestricted nvidiaPlanHostDriverBranch : Nat -- the bytes of NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS: 2 on the 570 branch -- (bEnable, bSkipSubmit), 3 from 580 (bSkipEnable added); the wrong size is -- NV_ERR_INVALID_ARGUMENT (0x1f), measured on an RTX A6000, 570.195.03 field unrestricted nvidiaPlanHostScheduleParamsSize : Nat -- Required location of a separately allocated direct-RM USERD buffer. -- Discrete Ampere needs video memory; the measured integrated GB10 path -- uses system memory. This is target policy, not a runtime retry choice. field unrestricted nvidiaPlanHostDirectUSERDMemory : (family NvidiaPlanHostMemory) field unrestricted nvidiaPlanHostDirectChannelFlags : Nat -- Direct-RM cache snooping is target policy. The GB10 bring-up's host-cached -- system buffers use 0x8010; the qualified Ampere path keeps 0x8000. See -- Memory.ABI.memoryABIDMAMappingFlags. A CPU publication barrier alone does -- not make a non-snooping GPU mapping coherent with cached CPU writes. field unrestricted nvidiaPlanHostDirectDMAFlags : Nat end-family -- one upload: bytes, or the contents of a file at run time family NvidiaPlanHostFills : Type 0 constructor NvidiaPlanHostFillsEnd constructor NvidiaPlanHostFillBytes field unrestricted nvidiaPlanHostFillHost : Nat field unrestricted nvidiaPlanHostFillPayload : Bytes recursive unrestricted nvidiaPlanHostFillsTail constructor NvidiaPlanHostFillFile field unrestricted nvidiaPlanHostFillFileHost : Nat field unrestricted nvidiaPlanHostFillFilePath : Bytes field unrestricted nvidiaPlanHostFillFileExtent : Nat recursive unrestricted nvidiaPlanHostFillFileTail end-family -- one readback: a host range written to stdout after completion family NvidiaPlanHostReads : Type 0 constructor NvidiaPlanHostReadsEnd constructor NvidiaPlanHostReadsNext field unrestricted nvidiaPlanHostReadHost : Nat field unrestricted nvidiaPlanHostReadExtent : Nat recursive unrestricted nvidiaPlanHostReadsTail end-family family NvidiaPlanHostLifecycle : Type 0 constructor NvidiaPlanHostDirectRM constructor NvidiaPlanHostUVM field unrestricted nvidiaPlanHostExternalRangeBase : Nat field unrestricted nvidiaPlanHostExternalRangeExtent : Nat end-family -- How the host treats a driver status. Strict: every one is asserted zero -- (the executables). Probe: every one after the root client's is recorded -- and none asserted, so a host on a card reports which call refused instead -- of stopping at it (the channel probe). The card-name and driver-branch -- assertions hold in both: a probe against the wrong card, or a driver -- whose ABI the host was not built for, stops. family NvidiaPlanHostMode : Type 0 constructor NvidiaPlanHostStrict constructor NvidiaPlanHostProbe end-family family NvidiaPlanHostLayout : Type 0 constructor NvidiaPlanHostLayoutValue field unrestricted nvidiaPlanHostGPFIFO : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostPushbuffer : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostSemaphores : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostProgram : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostQMD : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostUSERD : (family NvidiaPlanHostBuffer) field unrestricted nvidiaPlanHostData : (family NvidiaPlanHostBuffers) field unrestricted nvidiaPlanHostABI : (family NvidiaPlanHostABI) field unrestricted nvidiaPlanHostLifecycle : (family NvidiaPlanHostLifecycle) field unrestricted nvidiaPlanHostExpectedName : Bytes -- the host address the error notifier page is mapped at, 0 = not mapped field unrestricted nvidiaPlanHostErrorHost : Nat end-family -- The 570 branch: the 56-byte NVOS46 (the layout the retired 575 ABI of -- the RTX 3070 fixtures used) and the 2-byte schedule parameters. The 575 -- branch is no longer offered for any sm_86 card on RunPod (2026-09-24: -- 570.195, 580.65 .. 580.178, 595.91), so its ABI could not be qualified -- again and was retired; this one is qualified on an RTX A6000, 570.195.03. def nvidiaPlanHostAmpere570 : (family NvidiaPlanHostABI) = (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0384657 56 40 48 0xC56F 0xC7C0 0xC561 0 0x2E303735 2 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000) def nvidiaPlanHostAmpere580 : (family NvidiaPlanHostABI) = (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC56F 0xC7C0 0xC561 0 0x2E303835 3 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000) -- The DGX Spark's GB10 (compute 12.1) on the 580 branch: the 580 DMA-map ABI -- above with the classes this GPU's class list offers and the ladder -- allocated (tools/dgx/rung_tsg.py, rung_execute.py): BLACKWELL_CHANNEL_GPFIFO_A -- 0xC96F, BLACKWELL_COMPUTE_B 0xCEC0, HOPPER_USERMODE_A 0xC661. def nvidiaPlanHostBlackwell580 : (family NvidiaPlanHostABI) = (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC96F 0xCEC0 0xC661 0 0x2E303835 3 -- USERD in system memory (the GB10's channel buffers, Coppelius.Build. -- NativeHost), the channel flags every UVM plan allocates with, and the -- direct-RM DMA flags, which a UVM plan never reads (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory) 0x01000000 0x8000) -- A layout built for another driver ABI: every buffer, the lifecycle and -- the expected card unchanged, only the ABI (the DMA-map parameters, the -- classes, the driver branch it demands) replaced. def nvidiaPlanHostWithABI = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted abi : (family NvidiaPlanHostABI) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostLayout)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data previous lifecycle expectedName errorHost . (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost))))) -- ---- operands and commands ---- def phWord = (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value)) def phImm = nativeLaunchRecipeImmediate def phSlot = nativeLaunchRecipeSlotValue def phStore = nativeLaunchRecipeStore def phDiscard : (family NativePhysicalResultBinding) = (constructor NativePhysicalResultBinding NativePhysicalDiscardResult) def phState = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (phWord offset))) def phLoad = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateLoad64 (phWord offset))) def phPayload : (family NativePhysicalOperand) = (constructor NativePhysicalOperand NativePhysicalPayloadAddress modelWord64Zero) def phArgs = (lambda unrestricted a0 : (family NativePhysicalOperand) . (lambda unrestricted a1 : (family NativePhysicalOperand) . (lambda unrestricted a2 : (family NativePhysicalOperand) . (lambda unrestricted a3 : (family NativePhysicalOperand) . (lambda unrestricted a4 : (family NativePhysicalOperand) . (lambda unrestricted a5 : (family NativePhysicalOperand) . (constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5))))))) def phArgs3 = (lambda unrestricted a0 : (family NativePhysicalOperand) . (lambda unrestricted a1 : (family NativePhysicalOperand) . (lambda unrestricted a2 : (family NativePhysicalOperand) . (phArgs a0 a1 a2 (phImm 0) (phImm 0) (phImm 0))))) def phIdentity : Bytes = b"nvidia-plan-host" def phNext = (lambda unrestricted operation : (family NativePhysicalOperation) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand operation phIdentity tail))) def phCall = (lambda unrestricted number : Nat . (lambda unrestricted argv : (family NativePhysicalArguments) . (lambda unrestricted payload : Bytes . (lambda unrestricted result : (family NativePhysicalResultBinding) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phImm number) argv payload result) tail)))))) def phCopy = (lambda unrestricted offset : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (phWord offset) (phWord (bytes-length payload)) payload) tail)))) -- Linux x86-64 def phSysRead : Nat = 0 def phSysWrite : Nat = 1 def phSysClose : Nat = 3 def phSysMmap : Nat = 9 def phSysIoctl : Nat = 16 def phSysDup2 : Nat = 33 def phSysExitGroup : Nat = 231 def phSysOpenat : Nat = 257 def phSysPipe2 : Nat = 293 def phAtFdCwd : Nat = 18446744073709551516 def phOpenFlags : Nat = 0x80002 def phMapAnonymousFixed : Nat = 0x32 def phMapSharedFixed : Nat = 0x11 def phNoDescriptor : Nat = 18446744073709551615 -- RM and UVM escapes def phRMAlloc : Nat = 0xC020462B def phRMControl : Nat = 0xC020462A def phRMMapMemory : Nat = 0xC038464E def phRMFree : Nat = 0xC0104629 def phRegisterFD : Nat = 0xC00446C9 def phWaitOpen : Nat = 0xC00846DA def phUVMInitialize : Nat = 0x30000001 def phUVMMMInitialize : Nat = 75 def phUVMRegisterGPU : Nat = 37 def phUVMRegisterGPUVASpace : Nat = 25 def phUVMRegisterChannel : Nat = 27 def phUVMCreateExternalRange : Nat = 73 def phUVMMapExternalAllocation : Nat = 33 def phUVMChannelRangeBase : Nat = 0xA00000000 def phUVMChannelRangeExtent : Nat = 0x4000000 -- result slots and fixed descriptors def phSlotControl : Nat = 0 def phSlotGPU : Nat = 1 def phSlotMap : Nat = 2 def phSlotFile : Nat = 3 -- slots 4..13 belong to the request host (PlanHostRequest), 14 and 15 to -- the native telemetry. Transfers own the next slot and never overwrite a -- request file descriptor or a mapping result while checking short I/O. def phSlotTransfer : Nat = 16 def phSlots : Nat = (succ phSlotTransfer) def phFdControl : Nat = 100 def phFdCard : Nat = 101 def phFdMap : Nat = 102 def phFdUVM : Nat = 103 def phFdUVMMemoryMap : Nat = 104 -- RM handles, caller-chosen for children def phHDevice : Nat = 0xDEAD0080 def phHSubdevice : Nat = 0xDEAD2080 def phHVASpace : Nat = 0xDEAD90F1 def phHError : Nat = 0xDEAD0E44 def phHGroup : Nat = 0xDEADA06C def phHContext : Nat = 0xDEAD9067 def phHDMA : Nat = 0xDEAD0070 def phHMemory = (lambda unrestricted index : Nat . (naturalAdd 0xB0000000 index)) def phHVirtual = (lambda unrestricted index : Nat . (naturalAdd 0xB1000000 index)) def phHClass = (lambda unrestricted class : Nat . (naturalAdd 0xDEAD0000 class)) -- state layout, 16 KiB: RM call blocks, then a 16-byte status record per -- buffer, then 256 bytes of call blocks per buffer (at most 24 buffers, to -- 10240); the request host's areas follow (PlanHostRequest) def phStateExtent : Nat = 16384 def phBufferBlocksEnd : Nat = 10240 def phRoot : Nat = 0 def phDev : Nat = 64 def phSub : Nat = 128 def phVAS : Nat = 192 def phErrMap : Nat = 256 def phErr : Nat = 2048 def phGroup : Nat = 2112 def phCtx : Nat = 2176 def phChan : Nat = 2240 def phComp : Nat = 2304 def phUser : Nat = 2368 def phBind : Nat = 2432 def phSched : Nat = 2496 def phTok : Nat = 2560 def phDoorMap : Nat = 2624 def phWait : Nat = 2688 def phPipe : Nat = 2752 def phScratch : Nat = 2816 def phName : Nat = 2880 def phPreempt : Nat = 3008 def phFree : Nat = 3040 def phDMAObject : Nat = 3072 def phUVMControl : Nat = 3136 def phBufferState = (lambda unrestricted index : Nat . (naturalAdd 4096 (naturalMultiply index 256))) def phBufferStatus = (lambda unrestricted index : Nat . (naturalAdd 3200 (naturalMultiply index 16))) def phBuffersMaximum : Nat = 24 -- the fixed anonymous parameter page, 64 KiB def phParams : Nat = 0x50000000 def phDevP : Nat = 0x50000000 def phSubP : Nat = 0x50000100 def phVASP : Nat = 0x50000200 def phErrP : Nat = 0x50001100 def phGroupP : Nat = 0x50001200 def phCtxP : Nat = 0x50001300 def phChanP : Nat = 0x50001400 def phBindP : Nat = 0x50001600 def phSchedP : Nat = 0x50001700 def phTokP : Nat = 0x50001800 def phRegFdP : Nat = 0x50001980 def phPreemptP : Nat = 0x50001A00 def phNameP : Nat = 0x50001B00 def phMemP = (lambda unrestricted index : Nat . (naturalAdd 0x50002000 (naturalMultiply index 0x200))) def phVirtP = (lambda unrestricted index : Nat . (naturalAdd 0x50002100 (naturalMultiply index 0x200))) def phDMAObjectP : Nat = 0x50007F00 def phUVMGidP : Nat = 0x50008000 def phUVMInitP : Nat = 0x50008200 def phUVMMMP : Nat = 0x50008300 def phUVMRegisterGPUP : Nat = 0x50008400 def phUVMRegisterVASpaceP : Nat = 0x50008500 def phUVMRegisterChannelP : Nat = 0x50008600 def phUVMCreateRangeP : Nat = 0x50008700 def phUVMMapAllocationP : Nat = 0x50009000 def phDoorHost : Nat = 0x60800000 def phStatusSentinel : Nat = 0xFFFFFFFF -- ---- little-endian blocks ---- def phZeros = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . Bytes) b"" (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction))) count)) def phDrop = dataBytesDropValidated def phTake = dataBytesTakeValidated def phW32 = (lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value))) def phW64 = (lambda unrestricted value : Nat . (dataBytesWord64LE (phWord value))) def phSet = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted field : Bytes . (bytes-append (phTake offset block) (bytes-append field (phDrop (naturalAdd offset (bytes-length field)) block)))))) def phSet32 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW32 value))))) def phSet64 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW64 value))))) -- ---- the pipe memcpy ---- def phCopyStateToState = (lambda unrestricted destination : Nat . (lambda unrestricted source : Nat . (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) (phState source) (phImm count)) b"" phDiscard (phCall phSysRead (phArgs3 (phLoad phPipe) (phState destination) (phImm count)) b"" phDiscard tail)))))) -- A pipe is not an unbounded staging buffer. A single-threaded write/read -- pair deadlocks when its write exceeds capacity (the matrix qualification -- stopped in write(901120), after filling 65536 bytes). Drain every bounded -- chunk before writing another. Linux PIPE_BUF is 4096 on both target ABIs; -- the empty pipe admits that atomic extent even when capacity is one page. -- Short/error returns fail by name, including interruption; no partial copy -- is reported as a successful upload. Result slot ownership is explicit. def phPipeChunkBytes : Nat = 4096 def phPipeChunkCount = (lambda unrestricted count : Nat . (naturalAdd (naturalDivideUnchecked count phPipeChunkBytes) (naturalNonzero (naturalModuloUnchecked count phPipeChunkBytes)))) def phPipeChunk = (lambda unrestricted source : (family NativePhysicalOperand) . (lambda unrestricted destination : (family NativePhysicalOperand) . (lambda unrestricted count : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) source (phImm count)) payload (phStore phSlotTransfer) (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-write" (phCall phSysRead (phArgs3 (phLoad phPipe) destination (phImm count)) b"" (phStore phSlotTransfer) (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-read" tail))))))))) def phFill = (lambda unrestricted address : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (app (nat-eliminate (lambda unrestricted remaining : Nat . (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands)))) (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . tail)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))) . (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . (let unrestricted count = (naturalMinimum phPipeChunkBytes (bytes-length bytes)) in (phPipeChunk phPayload (phImm at) count (dataBytesTakeValidated count bytes) (induction (naturalAdd at count) (dataBytesDropValidated count bytes)))))))) (phPipeChunkCount (bytes-length payload))) address payload)))) -- Address-based copies share the same transfer/check mechanism. Their -- ranges must be disjoint as before; this is not an overlapping memmove. def phPipeRanges = (lambda unrestricted source : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) . (lambda unrestricted destination : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) . (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted chunks = (phPipeChunkCount count) in (nat-eliminate (lambda unrestricted i : Nat . (family NativePhysicalCommands)) tail (lambda unrestricted index : Nat . (lambda unrestricted rest : (family NativePhysicalCommands) . (let unrestricted offset = (naturalMultiply (naturalSaturatingSubtract chunks (succ index)) phPipeChunkBytes) in (phPipeChunk (source offset) (destination offset) (naturalMinimum phPipeChunkBytes (naturalSaturatingSubtract count offset)) b"" rest)))) chunks)))))) def phCopyMappedToState = (lambda unrestricted address : Nat . (lambda unrestricted destination : Nat . (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset))) (lambda unrestricted offset : Nat . (phState (naturalAdd destination offset)))))) def phCopyStateToMapped = (lambda unrestricted source : Nat . (lambda unrestricted address : Nat . (phPipeRanges (lambda unrestricted offset : Nat . (phState (naturalAdd source offset))) (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset)))))) def phCopyMappedToMapped = (lambda unrestricted source : Nat . (lambda unrestricted destination : Nat . (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd source offset))) (lambda unrestricted offset : Nat . (phImm (naturalAdd destination offset)))))) -- the pipe the memcpys above go through; every entry point creates it first def phPipeCreate = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysPipe2 (phArgs3 (phState phPipe) (phImm 0) (phImm 0)) b"" phDiscard tail)) -- Read the declared prefix into a mapped buffer. Short reads (including -- interruption), missing files and I/O errors fail before later uploads or -- submissions; an unread suffix is allowed by this fill's prefix contract. -- Keep the descriptor in phScratch while phSlotFile carries read/close -- results. Both are owned temporaries across this straight-line fragment; -- no caller's request or telemetry slot is borrowed. Closing also prevents -- a multi-tensor import from exhausting the process's file descriptors. -- Bytes has an explicit extent; openat requires a terminating zero. An -- eight-byte path otherwise runs into the next payload in the host image. -- Caller-supplied trailing zeros remain harmless; never rely on pool padding. def phReadFile = (lambda unrestricted path : Bytes . (lambda unrestricted address : Nat . (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm 0)) (bytes-append path b"\x00") (phStore phSlotFile) (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState phScratch) (phSlot phSlotFile)) (phCall phSysRead (phArgs3 (phSlot phSlotFile) (phImm address) (phImm count)) b"" (phStore phSlotFile) (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm count) b"input-file-read" (phCall phSysClose (phArgs3 (phLoad phScratch) (phImm 0) (phImm 0)) b"" (phStore phSlotFile) (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm 0) b"input-file-close" tail)))))))))) def phRangeBase = (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle (branch NvidiaPlanHostDirectRM . 0) (branch NvidiaPlanHostUVM base extent . base))) def phRangeExtent = (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle (branch NvidiaPlanHostDirectRM . 0) (branch NvidiaPlanHostUVM base extent . extent))) -- 1 when the buffer lies inside the lifecycle's pre-created external range, -- the video arena: such a buffer is mapped into the range, not given one def phInsideRange = (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (lambda unrestricted gpu : Nat . (lambda unrestricted extent : Nat . (naturalAnd (naturalNonzero (phRangeExtent lifecycle)) (naturalAnd (naturalLessOrEqual (phRangeBase lifecycle) gpu) (naturalLessOrEqual (naturalAdd gpu extent) (naturalAdd (phRangeBase lifecycle) (phRangeExtent lifecycle)))))))) def phWhen = (lambda unrestricted flag : Nat . (lambda unrestricted commands : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalCommands)) tail (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (commands tail))) flag)))) -- ---- fail closed ---- def phAssertStateZero32 = (lambda unrestricted identity : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy phScratch (phZeros 8) (phCopyStateToState phScratch offset 4 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail)))))) def phAssertMappedZero32 = (lambda unrestricted identity : Bytes . (lambda unrestricted address : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy phScratch (phZeros 8) (phCopyMappedToState address phScratch 4 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail)))))) -- the same, unless tolerated def phCheckStateZero32 = (lambda unrestricted identity : Bytes . (lambda unrestricted tolerate : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phWhen (naturalIsZero tolerate) (phAssertStateZero32 identity offset) tail))))) def phCheckMappedZero32 = (lambda unrestricted identity : Bytes . (lambda unrestricted tolerate : Nat . (lambda unrestricted address : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phWhen (naturalIsZero tolerate) (phAssertMappedZero32 identity address) tail))))) -- ---- RM alloc / control, each asserted ---- def phAlloc = (lambda unrestricted identity : Bytes . (lambda unrestricted tolerate : Nat . (lambda unrestricted block : Nat . (lambda unrestricted parent : Nat . (lambda unrestricted class : Nat . (lambda unrestricted paramsAddress : Nat . (lambda unrestricted paramsSize : Nat . (lambda unrestricted handle : Nat . (lambda unrestricted statusOffset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 parent) 8 handle) 12 class) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel) (phCopyStateToState block (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState block)) b"" phDiscard (phCopyStateToState statusOffset (naturalAdd block 28) 4 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail))))))))))))))) def phControl = (lambda unrestricted identity : Bytes . (lambda unrestricted tolerate : Nat . (lambda unrestricted statusOffset : Nat . (lambda unrestricted block : Nat . (lambda unrestricted object : Nat . (lambda unrestricted command : Nat . (lambda unrestricted paramsAddress : Nat . (lambda unrestricted paramsSize : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 object) 8 command) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel) (phCopyStateToState block (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMControl) (phState block)) b"" phDiscard (phCopyStateToState statusOffset (naturalAdd block 28) 4 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail)))))))))))))) -- a UVM ioctl whose status word lives in its parameter block: the word is -- recorded in the UVM status record, one 4-byte slot per call, and asserted -- zero unless the call is one the proven hosts tolerate a non-zero from def phUVMStatusRecord : Nat = 3584 def phUVMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd phUVMStatusRecord (naturalMultiply slot 4))) def phUVMStatusRecordExtent : Nat = 512 -- RM status record slots after the UVM slots def phRMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd 4000 (naturalMultiply slot 4))) -- the `tolerate` an RM alloc or control takes under a mode def phTolerate = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (eliminate NvidiaPlanHostMode (lambda unrestricted current : (family NvidiaPlanHostMode) . Nat) mode (branch NvidiaPlanHostStrict . 0) (branch NvidiaPlanHostProbe . 1))) def phUVMCall = (lambda unrestricted identity : Bytes . (lambda unrestricted slot : Nat . (lambda unrestricted tolerate : Nat . (lambda unrestricted descriptor : Nat . (lambda unrestricted request : Nat . (lambda unrestricted paramsAddress : Nat . (lambda unrestricted statusOffset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysIoctl (phArgs3 (phImm descriptor) (phImm request) (phImm paramsAddress)) b"" phDiscard (phCopyMappedToState (naturalAdd paramsAddress statusOffset) (phUVMStatusSlot slot) 4 (phCheckMappedZero32 identity tolerate (naturalAdd paramsAddress statusOffset) tail))))))))))) -- the same, right after the UVM device was opened onto `descriptor`: the -- dup2 that placed it returned `descriptor` (it returns a negative errno -- when the open failed), or -- unless `openTolerate` -- the host stops with -- `uvm-open`, not at the ioctl that finds no device behind the descriptor. -- Measured on RunPod, 2026-09-24: a container whose /dev/nvidia-uvm exists -- but opens with EIO used to stop at `uvm-initialize`. def phUVMCallAfterOpen = (lambda unrestricted openTolerate : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted slot : Nat . (lambda unrestricted tolerate : Nat . (lambda unrestricted descriptor : Nat . (lambda unrestricted request : Nat . (lambda unrestricted paramsAddress : Nat . (lambda unrestricted statusOffset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phWhen (naturalIsZero openTolerate) (nativeLaunchRecipeAssertEqual (phSlot phSlotMap) (phImm descriptor) b"uvm-open") (phUVMCall identity slot tolerate descriptor request paramsAddress statusOffset tail))))))))))) -- ---- buffers ---- def phBufferGPU = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . gpu))) def phBufferHost = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . host))) def phBufferExtent = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . extent))) def phBufferIsVideo = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory (branch NvidiaPlanHostSystemMemory . 0) (branch NvidiaPlanHostVideoMemory . 1) (branch NvidiaPlanHostPagedSystemMemory . 0) (branch NvidiaPlanHostGPUCachedSystemMemory . 0))))) def phBufferIsPaged = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory (branch NvidiaPlanHostSystemMemory . 0) (branch NvidiaPlanHostVideoMemory . 0) (branch NvidiaPlanHostPagedSystemMemory . 1) (branch NvidiaPlanHostGPUCachedSystemMemory . 0))))) def phBufferIsGPUCached = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory (branch NvidiaPlanHostSystemMemory . 0) (branch NvidiaPlanHostVideoMemory . 0) (branch NvidiaPlanHostPagedSystemMemory . 0) (branch NvidiaPlanHostGPUCachedSystemMemory . 1))))) def phABI = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted which : Nat . (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags . (naturalSelect (naturalEqual which 0) mapDMA (naturalSelect (naturalEqual which 1) size (naturalSelect (naturalEqual which 2) dmaOffset (naturalSelect (naturalEqual which 3) status (naturalSelect (naturalEqual which 4) channel (naturalSelect (naturalEqual which 5) compute (naturalSelect (naturalEqual which 6) usermode (naturalSelect (naturalEqual which 7) engine (naturalSelect (naturalEqual which 8) driverBranch (naturalSelect (naturalEqual which 9) scheduleSize channelFlags)))))))))))))) def phUSERDRequiresVideo = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags . (eliminate NvidiaPlanHostMemory (lambda unrestricted memory : (family NvidiaPlanHostMemory) . Nat) userdMemory (branch NvidiaPlanHostSystemMemory . 0) (branch NvidiaPlanHostVideoMemory . 1) (branch NvidiaPlanHostPagedSystemMemory . 0) (branch NvidiaPlanHostGPUCachedSystemMemory . 0))))) def phIsUVM = (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle (branch NvidiaPlanHostDirectRM . 0) (branch NvidiaPlanHostUVM base extent . 1))) -- a buffer extent for a table: the table's bytes rounded up to a unit def nvidiaPlanHostRoundUp = (lambda unrestricted value : Nat . (lambda unrestricted unit : Nat . (naturalMultiply (naturalDivideUnchecked (naturalAdd value (naturalSaturatingSubtract unit 1)) unit) unit))) -- Where the host may write: the host-mapped buffers of a layout (host 0 = -- not mapped), the error notifier's page among them. A range is admitted -- when mapped buffers cover it end to end -- adjacent mappings may carry -- one table across their seam (Coppelius's QMD primary and overflow). def nvidiaPlanHostErrorPageBytes : Nat = 0x1000 def phMapped = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted rest : (family NvidiaPlanHostBuffers) . (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext buffer rest))) def phLayoutMappings = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd (phMapped userd (phMapped (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue b"error-notifier" 0 errorHost nvidiaPlanHostErrorPageBytes (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)) data)))))))))) def phMappingCount = (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers (branch NvidiaPlanHostBuffersEnd . 0) (branch NvidiaPlanHostBuffersNext head rest induction . (succ induction)))) -- the end of the first host-mapped buffer holding the byte at `host`, 0 when none does def phMappingEndAt = (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (lambda unrestricted host : Nat . (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers (branch NvidiaPlanHostBuffersEnd . 0) (branch NvidiaPlanHostBuffersNext head rest induction . (naturalSelect (naturalAnd (naturalNonzero (phBufferHost head)) (naturalAnd (naturalLessOrEqual (phBufferHost head) host) (naturalLess host (naturalAdd (phBufferHost head) (phBufferExtent head))))) (naturalAdd (phBufferHost head) (phBufferExtent head)) induction))))) -- 1 when the buffers cover [host, host + extent): step from mapping to -- mapping, at most once per mapping (the fuel) def phCovers = (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (lambda unrestricted fuel : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat))) (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (naturalEqual extent 0))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)) . (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (let unrestricted end = (phMappingEndAt buffers host) in (naturalSelect (naturalEqual extent 0) 1 (naturalSelect (naturalEqual end 0) 0 (induction end (naturalSaturatingSubtract (naturalAdd host extent) end))))))))) fuel))) def nvidiaPlanHostContains = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (let unrestricted mappings = (phLayoutMappings layout) in (phCovers mappings (phMappingCount mappings) host extent))))) -- a GPU-cached buffer is CPU-uncached (MAP_NOT_REQUIRED): no host address def phGPUCachedUnmapped = (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers (branch NvidiaPlanHostBuffersEnd . 1) (branch NvidiaPlanHostBuffersNext head rest induction . (naturalAnd induction (naturalSelect (phBufferIsGPUCached head) (naturalIsZero (phBufferHost head)) 1))))) -- Admission, 1 when the host will be derived: under direct-RM the USERD -- buffer has the target ABI's location (Ampere requires video memory; -- the integrated GB10 profile requires system memory). Under -- UVM the USERD entry is the alias of the GPFIFO's last page and is not -- allocated, so there is nothing to admit. A pairing gates its artifact -- on this and the checker decides it. def nvidiaPlanHostLayoutAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (naturalAnd (phGPUCachedUnmapped (phLayoutMappings layout)) (naturalSelect (phIsUVM lifecycle) 1 (naturalEqual (phBufferIsVideo userd) (phUSERDRequiresVideo abi))))))) -- ---- the layout's placement certificate ---- -- Every buffer of a layout is a resident of two arenas: the card's virtual -- address space (49 bits on Ampere) at its GPU address, and the process's -- (47 bits of user space) at its host address when it is mapped there. In -- each, Runtime.ArenaCertificate decides every resident page-aligned, -- non-empty, inside, and disjoint from every other -- PlanHost's own fixed -- mappings (the parameter page, the doorbell) and, under UVM, the channel's -- range among them. The one sanctioned alias, the UVM USERD entry (the -- GPFIFO buffer's last page, never allocated), is not a resident: it must -- lie inside the GPFIFO buffer in both spaces. def nvidiaPlanHostPageBytes : Nat = 0x1000 def phGPUSpaceBytes : Nat = 0x2_0000_0000_0000 def phHostSpaceBytes : Nat = 0x8000_0000_0000 def phResident = (lambda unrestricted identity : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted rest : (family ArenaResidents) . (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue identity offset extent nvidiaPlanHostPageBytes) rest))))) -- a buffer at its GPU address def phGPUResident = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted rest : (family ArenaResidents) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (phResident identity gpu extent rest))))) -- a buffer at its host address, when it is mapped (host 0 = not mapped) def phHostResident = (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted rest : (family ArenaResidents) . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents)) rest (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) . (phResident identity host extent rest))) (naturalNonzero host)))))) def phEachResident = (lambda unrestricted place : (pi unrestricted buffer : (family NvidiaPlanHostBuffer) . (pi unrestricted rest : (family ArenaResidents) . (family ArenaResidents))) . (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (lambda unrestricted rest : (family ArenaResidents) . (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (family ArenaResidents)) buffers (branch NvidiaPlanHostBuffersEnd . rest) (branch NvidiaPlanHostBuffersNext head tail induction . (place head induction)))))) -- the layout's buffers, the USERD entry only when it is allocated (direct-RM) def phAllocatedBuffers = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd (nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostBuffers)) (phMapped userd data) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NvidiaPlanHostBuffers) . data)) (phIsUVM lifecycle)))))))))) def phGPUResidents = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (phEachResident phGPUResident (phAllocatedBuffers layout) (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family ArenaResidents)) lifecycle (branch NvidiaPlanHostDirectRM . (constructor ArenaResidents ArenaResidentsEnd)) (branch NvidiaPlanHostUVM base extent . (phResident b"uvm-channel-range" phUVMChannelRangeBase phUVMChannelRangeExtent (constructor ArenaResidents ArenaResidentsEnd)))))))) -- `extras`: the mappings a host adds of its own (the request host's recipe -- staging area) def phHostResidents = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted extras : (family ArenaResidents) . (phEachResident phHostResident (phAllocatedBuffers layout) (phResident b"parameters" phParams 0x10000 (phResident b"doorbell" phDoorHost 0x10000 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents)) extras (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) . (phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes extras))) (naturalNonzero errorHost))))))))) -- [inner, inner + innerExtent) inside [outer, outer + outerExtent) def phInside = (lambda unrestricted inner : Nat . (lambda unrestricted innerExtent : Nat . (lambda unrestricted outer : Nat . (lambda unrestricted outerExtent : Nat . (naturalAnd (naturalLessOrEqual outer inner) (naturalLessOrEqual (naturalAdd inner innerExtent) (naturalAdd outer outerExtent))))))) -- under UVM, the USERD entry inside the GPFIFO buffer in both spaces def phUSERDAliasInside = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (naturalSelect (phIsUVM lifecycle) (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) userd (branch NvidiaPlanHostBufferValue aliasIdentity aliasGPU aliasHost aliasExtent aliasMemory . (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) gpfifo (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (naturalAnd (phInside aliasGPU aliasExtent gpu extent) (phInside aliasHost aliasExtent host extent)))))) 1)))) -- 1 when the layout's placement is certified in both spaces def nvidiaPlanHostLayoutCertified = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted extras : (family ArenaResidents) . (naturalAnd (arenaCertificate phGPUSpaceBytes (phGPUResidents layout)) (naturalAnd (arenaCertificate phHostSpaceBytes (phHostResidents layout extras)) (phUSERDAliasInside layout))))) -- Every upload lands inside a host-mapped buffer of the layout: bytes, or a -- file's declared extent. The subagent's RTX 3070 sweep (2026-09-23) found -- program tables up to 7936 bytes built into a 4096-byte program buffer and -- copied past it at run time -- the kernel never ran; now the build refuses. def nvidiaPlanHostFillsAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted fills : (family NvidiaPlanHostFills) . (eliminate NvidiaPlanHostFills (lambda unrestricted current : (family NvidiaPlanHostFills) . Nat) fills (branch NvidiaPlanHostFillsEnd . 1) (branch NvidiaPlanHostFillBytes host payload rest induction . (naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction)) (branch NvidiaPlanHostFillFile host path extent rest induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction))))) -- what a plan-derived host needs admitted before it is built def nvidiaPlanHostAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted fills : (family NvidiaPlanHostFills) . (naturalAnd (nvidiaPlanHostLayoutAdmitted layout) (naturalAnd (nvidiaPlanHostLayoutCertified layout (constructor ArenaResidents ArenaResidentsEnd)) (nvidiaPlanHostFillsAdmitted layout fills))))) -- system memory: host-cached, contiguous or noncontiguous as declared. video memory: the local-user -- object, write-combined, contiguous, page-aligned. -- system memory's attributes: PCI, cached, and contiguous (0x32000000) or, -- paged, non-contiguous (0x2A000000) def phGPUCachedPageBytes : Nat = 0x10000 -- NV_MEMORY_ALLOCATION_PARAMS for a buffer: owner, flags (8), attr (24), -- attr2 (28), format (32), size (64), alignment (72), limit (88) def phGPUCachedMemoryParams = (lambda unrestricted extent : Nat . (phSet64 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 8 0x0000C001) 24 0x0B000000) 28 0x00000005) 32 0x00000006) 64 extent) 72 phGPUCachedPageBytes) 88 (naturalSaturatingSubtract extent 1))) def phMemoryParams = (lambda unrestricted video : Nat . (lambda unrestricted paged : Nat . (lambda unrestricted cached : Nat . (lambda unrestricted inside : Nat . (lambda unrestricted extent : Nat . (nat-eliminate (lambda unrestricted current : Nat . Bytes) (nat-eliminate (lambda unrestricted current : Nat . Bytes) (phSet64 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 24 (naturalSelect paged 0x2A000000 0x32000000)) 64 extent) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (phGPUCachedMemoryParams extent))) cached) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x48454C49) 8 0x00008000) 24 (naturalSelect inside 0x58000000 0x50000000)) 64 extent) 72 0x1000))) video)))))) def phMemoryClass = (lambda unrestricted video : Nat . (naturalSelect video 0x40 0x3E)) -- the host mapping of one buffer through a fresh control descriptor, or for -- video memory through a fresh card descriptor def phOpenCardsInto = (lambda unrestricted descriptor : Nat . (lambda unrestricted path : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotMap) (phCall phSysIoctl (phArgs3 (phSlot phSlotMap) (phImm phWaitOpen) (phState phWait)) b"" phDiscard (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm descriptor) (phImm 0)) b"" phDiscard tail)))))) def phMappingDescriptor = (lambda unrestricted video : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalCommands)) (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotMap) (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdMap) (phImm 0)) b"" phDiscard tail)) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (phOpenCardsInto phFdMap b"/dev/nvidia0\x00" (phOpenCardsInto phFdMap b"/dev/nvidia1\x00" (phOpenCardsInto phFdMap b"/dev/nvidia2\x00" (phOpenCardsInto phFdMap b"/dev/nvidia3\x00" (phOpenCardsInto phFdMap b"/dev/nvidia4\x00" (phOpenCardsInto phFdMap b"/dev/nvidia5\x00" (phOpenCardsInto phFdMap b"/dev/nvidia6\x00" (phOpenCardsInto phFdMap b"/dev/nvidia7\x00" tail)))))))))) video))) -- the host mapping of one RM memory object: the NVOS33 map through the -- fresh descriptor, its status recorded, then mmap at the host address def phMapMemory = (lambda unrestricted identity : Bytes . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted block : Nat . (lambda unrestricted hMemory : Nat . (lambda unrestricted video : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted host : Nat . (lambda unrestricted statusOffset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted flags = (naturalSelect video 0x01010000 0x03008000) in (phMappingDescriptor video (phCall phSysIoctl (phArgs3 (phImm phFdMap) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard (phCopy block (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 56) 4 phHDevice) 8 hMemory) 24 extent) 40 phStatusSentinel) 44 flags) 48 phFdMap) (phCopyStateToState block (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState block)) b"" phDiscard (phCopyStateToState statusOffset (naturalAdd block 40) 4 (phCheckStateZero32 identity (phTolerate mode) (naturalAdd block 40) (phCall phSysMmap (phArgs (phImm host) (phImm extent) (phImm 3) (phImm phMapSharedFixed) (phImm phFdMap) (phImm 0)) b"" phDiscard tail)))))))))))))))))) def phHostMap = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted index : Nat . (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phMapMemory b"host-map" mode (naturalAdd (phBufferState index) 128) (phHMemory index) (phBufferIsVideo buffer) (phBufferExtent buffer) (phBufferHost buffer) (naturalAdd (phBufferStatus index) 12) tail))))) def phDirectDMAFlags = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags . directDMAFlags))) -- direct-RM: a fixed virtual reservation and the DMA map to it def phDirectRange = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted index : Nat . (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted st = (phBufferState index) in (let unrestricted gpu = (phBufferGPU buffer) in (let unrestricted extent = (phBufferExtent buffer) in (phFill (phVirtP index) (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 (naturalSaturatingSubtract (naturalAdd gpu extent) 1)) 16 phHVASpace) (phAlloc b"alloc:virtual" (phTolerate mode) (naturalAdd st 32) phHDevice 0x70 (phVirtP index) 24 (phHVirtual index) (naturalAdd (phBufferStatus index) 4) (phCopy (naturalAdd st 64) (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros (phABI abi 1)) 4 phHDevice) 8 (phHVirtual index)) 12 (phHMemory index)) 32 (phDirectDMAFlags abi)) 24 extent) (phABI abi 2) gpu) (phABI abi 3) phStatusSentinel) (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4 (phCheckStateZero32 b"dma-map" (phTolerate mode) (naturalAdd st (naturalAdd 64 (phABI abi 3))) tail))))))))))))))) -- NVOS46 flags of the UVM path's DMA map: DMA_OFFSET_FIXED, CACHE_SNOOP, -- and 4 KiB pages; a GPU-cached buffer takes the allocation's own (64 KiB) -- page size instead def phUVMDMAFlags : Nat = 0x8110 def phUVMDMAFlagsDefaultPages : Nat = 0x8010 -- UVM: an external range at the plan's address, the DMA map through the -- device DMA selector, and the mapping registered with UVM def phUVMRange = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted inside : Nat . (lambda unrestricted index : Nat . (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted st = (phBufferState index) in (let unrestricted gpu = (phBufferGPU buffer) in (let unrestricted extent = (phBufferExtent buffer) in (let unrestricted tolerate = (phTolerate mode) in (phWhen (naturalIsZero inside) (lambda unrestricted rest : (family NativePhysicalCommands) . (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 extent) 16 phStatusSentinel) (phUVMCall b"uvm-buffer-range" (naturalAdd 8 (naturalMultiply 2 index)) tolerate phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest))) (phCopy (naturalAdd st 64) (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros (phABI abi 1)) 4 phHDevice) 8 phHDMA) 12 (phHMemory index)) 32 (naturalSelect (phBufferIsGPUCached buffer) phUVMDMAFlagsDefaultPages phUVMDMAFlags)) 24 extent) (phABI abi 2) gpu) (phABI abi 3) phStatusSentinel) (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4 (phCheckStateZero32 b"dma-map-uvm" tolerate (naturalAdd st (naturalAdd 64 (phABI abi 3))) (phFill phUVMMapAllocationP (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet64 (phSet64 (phZeros 9264) 0 gpu) 8 extent) 40 1) 9240 1) 9248 phFdControl) 9256 (phHMemory index)) 9260 phStatusSentinel) (phCopyMappedToMapped (naturalAdd phUVMGidP 12) (naturalAdd phUVMMapAllocationP 24) 16 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMMapAllocationP 9252) 4 (phUVMCall b"uvm-buffer-map" (naturalAdd 9 (naturalMultiply 2 index)) tolerate phFdUVM phUVMMapExternalAllocation phUVMMapAllocationP 9260 tail)))))))))))))))))))) -- One buffer: allocate, place, map. def phBuffer = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (lambda unrestricted index : Nat . (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted video = (phBufferIsVideo buffer) in (let unrestricted uvm = (phIsUVM lifecycle) in (let unrestricted inside = (phInsideRange lifecycle (phBufferGPU buffer) (phBufferExtent buffer)) in (phFill (phMemP index) (phMemoryParams video (phBufferIsPaged buffer) (phBufferIsGPUCached buffer) inside (phBufferExtent buffer)) (phAlloc b"alloc:buffer" (phTolerate mode) (phBufferState index) phHDevice (phMemoryClass video) (phMemP index) 128 (phHMemory index) (phBufferStatus index) (phWhen (naturalIsZero uvm) (phDirectRange abi mode index buffer) (phWhen uvm (phUVMRange abi mode inside index buffer) (phWhen (naturalNonzero (phBufferHost buffer)) (phHostMap mode index buffer) tail)))))))))))))) def phDataBuffers = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (lambda unrestricted first : Nat . (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) . (lambda unrestricted tail : (family NativePhysicalCommands) . (app (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (pi unrestricted index : Nat . (family NativePhysicalCommands))) buffers (branch NvidiaPlanHostBuffersEnd . (lambda unrestricted index : Nat . tail)) (branch NvidiaPlanHostBuffersNext head rest induction . (lambda unrestricted index : Nat . (phBuffer abi mode lifecycle index head (induction (succ index)))))) first))))))) -- ---- device discovery ---- def phOpenCard = (lambda unrestricted path : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotGPU) (phCall phSysIoctl (phArgs3 (phSlot phSlotGPU) (phImm phWaitOpen) (phState phWait)) b"" phDiscard (phCall phSysDup2 (phArgs3 (phSlot phSlotGPU) (phImm phFdCard) (phImm 0)) b"" phDiscard tail))))) def phDeviceProbe = (lambda unrestricted index : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phDevP (phSet32 (phZeros 56) 0 index) (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phDev)) b"" phDiscard tail)))) -- NV2080_CTRL_CMD_GPU_GET_NAME_STRING: the 64 ASCII bytes the card reports -- must equal the name the plan was paired with def phNameWord = (lambda unrestricted expected : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopyMappedToState (naturalAdd (naturalAdd phNameP 4) offset) phScratch 8 (phCopy (naturalAdd phScratch 8) (phTake 8 (phDrop offset expected)) (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phLoad (naturalAdd phScratch 8)) phIdentity tail)))))) def phExpectName = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted expected : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phNameP (phZeros 132) (phControl b"control:phName" (phTolerate mode) (phRMStatusSlot 11) phName phHSubdevice 0x20800110 phNameP 132 (phNameWord expected 0 (phNameWord expected 8 (phNameWord expected 16 (phNameWord expected 24 (phNameWord expected 32 (phNameWord expected 40 (phNameWord expected 48 (phNameWord expected 56 tail))))))))))))) -- ---- the UVM driver ---- def phUVMPrepare = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted base : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phUVMGidP (phSet32 (phSet32 (phZeros 268) 4 2) 8 16) (phControl b"control:phUVMControl" (phTolerate mode) (phRMStatusSlot 12) phUVMControl phHSubdevice 0x2080014A phUVMGidP 268 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap) (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVM) (phImm 0)) b"" (phStore phSlotMap) (phFill phUVMInitP (phSet32 (phZeros 16) 8 phStatusSentinel) (phUVMCallAfterOpen (phTolerate mode) b"uvm-initialize" 1 (phTolerate mode) phFdUVM phUVMInitialize phUVMInitP 8 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap) (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVMMemoryMap) (phImm 0)) b"" (phStore phSlotMap) (phFill phUVMMMP (phSet32 (phSet32 (phZeros 8) 0 phFdUVM) 4 phStatusSentinel) (phUVMCallAfterOpen (phTolerate mode) b"uvm-mm-initialize" 2 1 phFdUVMMemoryMap phUVMMMInitialize phUVMMMP 4 (phFill phUVMRegisterGPUP (phSet32 (phSet32 (phZeros 40) 24 phStatusSentinel) 36 phStatusSentinel) (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterGPUP 16 (phUVMCall b"uvm-register-gpu" 3 (phTolerate mode) phFdUVM phUVMRegisterGPU phUVMRegisterGPUP 36 (phFill phUVMRegisterVASpaceP (phSet32 (phSet32 (phSet32 (phZeros 32) 16 phFdControl) 24 phHVASpace) 28 phStatusSentinel) (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterVASpaceP 16 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterVASpaceP 20) 4 (phUVMCall b"uvm-register-vaspace" 4 (phTolerate mode) phFdUVM phUVMRegisterGPUVASpace phUVMRegisterVASpaceP 28 (phWhen (naturalNonzero extent) (lambda unrestricted rest : (family NativePhysicalCommands) . (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 base) 8 extent) 16 phStatusSentinel) (phUVMCall b"uvm-external-range" 6 (phTolerate mode) phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest))) tail)))))))))))))))))))))) def phUVMRegisterChannelCommands = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phUVMRegisterChannelP (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phZeros 56) 16 phFdControl) 24 (phHClass (phABI abi 4))) 32 phUVMChannelRangeBase) 40 phUVMChannelRangeExtent) 48 phStatusSentinel) (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterChannelP 16 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterChannelP 20) 4 (phUVMCall b"uvm-register-channel" 5 (phTolerate mode) phFdUVM phUVMRegisterChannel phUVMRegisterChannelP 48 tail))))))) -- ---- publishing a submission ---- -- gpPut into USERD, SFENCE, the work-submit token into the doorbell: the -- training runtime's publication routine (x86: mov [rdi], esi; sfence; -- mov [rdx], ecx), run on this thread, so the doorbell cannot reach the card -- ahead of gpPut through a write-combining buffer. The token is loaded -- from the parameter page into the scratch word first. -- -- Measured on an RTX 3090, driver 580.178.04, 2026-09-24. Before, gpPut -- went through the pipe copy and the doorbell after it, unordered: 7 hangs -- in 250 warp-sum runs, and in every one the semaphores were untouched (the -- device never began the pushbuffer), USERD's GP_PUT 1 and GP_GET 0 (the -- channel never fetched the entry) -- the doorbell had arrived before -- gpPut. A membarrier between the two (a locked-instruction barrier, which -- need not drain write-combining buffers) did not help: 11 hangs in 300 -- against 6 unfenced. This routine: 0 hangs in 300 against 13 unfenced, -- interleaved on the same card. def phPublishCode : Bytes = (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes) nativePhysicalTrainingGeneratePublish32Routine (branch X86NativeAssemblyEncoded code . code) (branch X86NativeAssemblyEncodeDuplicateLabel name . b"") (branch X86NativeAssemblyEncodeOffsetOverflow . b"") (branch X86NativeAssemblyMissingLabel name . b"") (branch X86NativeAssemblyDisplacementOutOfRange name . b"")) def phLoadToken = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy phScratch (phZeros 8) (phCopyMappedToState phTokP phScratch 4 tail))) def phPublishOperand = (lambda unrestricted userdGPPut : Nat . (lambda unrestricted gpPut : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine phPublishCode (phArgs (phImm userdGPPut) gpPut (phImm (naturalAdd phDoorHost 0x90)) (phLoad phScratch) (phImm 0) (phImm 0)) phDiscard) tail)))) def phPublish = (lambda unrestricted userdGPPut : Nat . (lambda unrestricted gpPut : Nat . (phPublishOperand userdGPPut (phImm gpPut)))) -- ---- the doorbell ---- def phDoorbell = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysIoctl (phArgs3 (phImm phFdCard) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard (phCopy phDoorMap (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 56) 4 phHSubdevice) 8 (phHClass (phABI abi 6))) 24 0x10000) 40 phStatusSentinel) 44 0) 48 phFdCard) (phCopyStateToState phDoorMap (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState phDoorMap)) b"" phDiscard (phCopyStateToState (phRMStatusSlot 18) (naturalAdd phDoorMap 40) 4 (phCheckStateZero32 b"doorbell-map" (phTolerate mode) (naturalAdd phDoorMap 40) (phCall phSysMmap (phArgs (phImm phDoorHost) (phImm 0x10000) (phImm 3) (phImm phMapSharedFixed) (phImm phFdCard) (phImm 0)) b"" phDiscard tail)))))))))) def phToken = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phTokP (phZeros 4) (phControl b"control:phTok" (phTolerate mode) (phRMStatusSlot 15) phTok (phHClass (phABI abi 4)) 0xc36f0108 phTokP 4 tail))))) def phSchedule = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phSchedP (phTake (phABI abi 9) (bytes 1 0 0)) (phControl b"control:phSched" (phTolerate mode) (phRMStatusSlot 14) phSched phHGroup 0xa06c0101 phSchedP (phABI abi 9) tail))))) def phVASpaceParams = (lambda unrestricted uvm : Nat . (nat-eliminate (lambda unrestricted current : Nat . Bytes) (phZeros 48) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (phSet64 (phSet64 (phSet32 (phZeros 48) 4 0x48) 8 0x1FFFFFB000000) 40 0x1000))) uvm)) def phUVMLifecycle = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family NativePhysicalCommands)) lifecycle (branch NvidiaPlanHostDirectRM . tail) (branch NvidiaPlanHostUVM base extent . (phUVMPrepare mode base extent tail)))))) def phDMASelector = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phDMAObjectP (phSet64 (phZeros 24) 8 0x1FFFFFFFFFFFF) (phAlloc b"alloc:phDMAObject" (phTolerate mode) phDMAObject phHDevice 0x70 phDMAObjectP 24 phHDMA (phRMStatusSlot 2) tail)))) def phDirectActivate = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phFill phBindP (phW32 1) (phControl b"control:phBind" (phTolerate mode) (phRMStatusSlot 13) phBind (phHClass (phABI abi 4)) 0xa06f0104 phBindP 4 (phSchedule abi mode (phToken abi mode (phDoorbell abi mode tail)))))))) def phUVMActivate = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phDoorbell abi mode (phFill phPreemptP (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 0 1) 4 phHGroup) 8 0) 12 2) (phControl b"control:phPreempt" (phTolerate mode) (phRMStatusSlot 16) phPreempt phHSubdevice 0x20801210 phPreemptP 32 (phToken abi mode (phUVMRegisterChannelCommands abi mode (phSchedule abi mode tail))))))))) -- the UVM lifecycle's GPFIFO: 0x8000 entries of 8 bytes in the video GPFIFO -- buffer, USERD the page after them def nvidiaPlanHostUVMGPFIFOEntries : Nat = 0x8000 def nvidiaPlanHostUVMGPFIFOBytes : Nat = (naturalMultiply nvidiaPlanHostUVMGPFIFOEntries 8) -- Where a plan maps its buffers in the process: from the origin, each -- after the previous at the alignment, in extents of the mapping unit. -- The host side of the arena certificate decides that they are disjoint -- and clear of the host's own mappings. def nvidiaPlanHostMappingOrigin : Nat = 0x6000_0000 def nvidiaPlanHostMappingAlignment : Nat = 0x0200_0000 def nvidiaPlanHostMappingUnit : Nat = 0x10000 -- the USERD page mapped after the GPFIFO entries, and the words of it the -- host reads: GP_GET and GP_PUT (Accelerator.SM86.USERD's layout, slot 0) def nvidiaPlanHostUSERDBytes : Nat = nvidiaPlanHostPageBytes def nvidiaPlanHostUSERDGPGetOffset : Nat = 0x88 def nvidiaPlanHostUSERDGPPutOffset : Nat = 0x8c def nvidiaPlanHostDirectGPFIFOEntries : Nat = 0x400 def phChannelParams = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted direct : Nat . (lambda unrestricted gpfifoGPU : Nat . (phSet32 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 368) 0 phHError) 4 (phHMemory 0)) 8 gpfifoGPU) 16 (naturalSelect direct nvidiaPlanHostDirectGPFIFOEntries nvidiaPlanHostUVMGPFIFOEntries)) 20 (naturalSelect direct (phABI abi 10) 0)) 24 phHContext) 32 (naturalSelect direct (phHMemory 5) (phHMemory 0))) 64 (naturalSelect direct 0 nvidiaPlanHostUVMGPFIFOBytes)) 128 (phABI abi 7))))) -- ---- the driver's branch ---- -- NV_ESC_CHECK_VERSION_STR (0xD2, 72 bytes: cmd, reply, 64 version bytes) -- with cmd '2', query: the driver writes its own version string. Its first -- four bytes must be the branch the host's ABI was built for, or the host -- stops, naming `driver-branch`, before any card call -- a 580-ABI host on a -- 575 driver used to run until its DMA map failed (exit 120 at `dma-map`), -- and on a 570 driver it faulted. Measured on the RTX 3090, 2026-09-24: -- driver 580.178.04 answers `580.178.04`, reply 1. A driver that does not -- answer leaves the bytes zero and is refused the same way. def phCheckVersionIoctl : Nat = 0xC04846D2 def phVersion : Nat = 1024 def phRootAndDriverBranch = (lambda unrestricted abi : (family NvidiaPlanHostABI) . (lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phAssertStateZero32 b"root" offset (phCopy phVersion (phSet32 (phZeros 72) 0 0x32) (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phCheckVersionIoctl) (phState phVersion)) b"" phDiscard (phCopy phScratch (phZeros 8) (phCopyStateToState phScratch (naturalAdd phVersion 8) 4 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm (phABI abi 8)) b"driver-branch" tail))))))))) -- ---- the prelude: a working compute channel ---- def phPrelude = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NativePhysicalCommands)) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (let unrestricted uvm = (phIsUVM lifecycle) in (let unrestricted direct = (naturalIsZero uvm) in (let unrestricted channelClass = (phHClass (phABI abi 4)) in (let unrestricted tolerate = (phTolerate mode) in (phOpenCard b"/dev/nvidia0\x00" (phOpenCard b"/dev/nvidia1\x00" (phOpenCard b"/dev/nvidia2\x00" (phOpenCard b"/dev/nvidia3\x00" (phOpenCard b"/dev/nvidia4\x00" (phOpenCard b"/dev/nvidia5\x00" (phOpenCard b"/dev/nvidia6\x00" (phOpenCard b"/dev/nvidia7\x00" (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotControl) (phCall phSysDup2 (phArgs3 (phSlot phSlotControl) (phImm phFdControl) (phImm 0)) b"" phDiscard (phCopy phRoot (phSet32 (phZeros 32) 28 phStatusSentinel) (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phRoot)) b"" phDiscard (phCopyStateToState (phRMStatusSlot 0) (naturalAdd phRoot 28) 4 (phRootAndDriverBranch abi (naturalAdd phRoot 28) (phCall phSysMmap (phArgs (phImm phParams) (phImm 0x10000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard (phFill phRegFdP (phW32 phFdControl) (phCopy phDev (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 8 phHDevice) 12 0x80) 16 phDevP) 24 56) (phCopyStateToState phDev (naturalAdd phRoot 8) 4 (phCopyStateToState (naturalAdd phDev 4) (naturalAdd phRoot 8) 4 (phDeviceProbe 0 (phDeviceProbe 1 (phDeviceProbe 2 (phDeviceProbe 3 (phDeviceProbe 4 (phDeviceProbe 5 (phDeviceProbe 6 (phDeviceProbe 7 (phFill phSubP (phZeros 4) (phAlloc b"alloc:phSub" tolerate phSub phHDevice 0x2080 phSubP 4 phHSubdevice (phRMStatusSlot 1) (phWhen (naturalNonzero (bytes-length expectedName)) (phExpectName mode expectedName) (phWhen uvm (phDMASelector mode) (phFill phVASP (phVASpaceParams uvm) (phAlloc b"alloc:phVAS" tolerate phVAS phHDevice 0x90f1 phVASP 48 phHVASpace (phRMStatusSlot 3) (phUVMLifecycle mode lifecycle (phBuffer abi mode lifecycle 0 gpfifo (phBuffer abi mode lifecycle 1 push (phBuffer abi mode lifecycle 2 sem (phBuffer abi mode lifecycle 3 program (phBuffer abi mode lifecycle 4 qmd (phWhen direct (phBuffer abi mode lifecycle 5 userd) (phDataBuffers abi mode lifecycle 6 data (phFill phErrP (phMemoryParams 0 0 0 0 0x1000) (phAlloc b"alloc:phErr" tolerate phErr phHDevice 0x3E phErrP 128 phHError (phRMStatusSlot 4) (phWhen (naturalNonzero errorHost) (phMapMemory b"error-map" mode phErrMap phHError 0 0x1000 errorHost (phRMStatusSlot 7)) (phFill phGroupP (phSet32 (phSet32 (phZeros 20) 8 (naturalSelect direct phHVASpace 0)) 12 1) (phAlloc b"alloc:phGroup" tolerate phGroup phHDevice 0xa06c phGroupP 20 phHGroup (phRMStatusSlot 5) (phFill phCtxP (phSet32 (phSet32 (phZeros 12) 0 phHVASpace) 4 uvm) (phAlloc b"alloc:phCtx" tolerate phCtx phHGroup 0x9067 phCtxP 12 phHContext (phRMStatusSlot 6) (phFill phChanP (phChannelParams abi direct (phBufferGPU gpfifo)) (phAlloc b"alloc:phChan" tolerate phChan phHGroup (phABI abi 4) phChanP 368 channelClass (phRMStatusSlot 8) (phAlloc b"alloc:phComp" tolerate phComp channelClass (phABI abi 5) 0 0 (phHClass (phABI abi 5)) (phRMStatusSlot 9) (phAlloc b"alloc:phUser" tolerate phUser phHSubdevice (phABI abi 6) 0 0 (phHClass (phABI abi 6)) (phRMStatusSlot 10) (phWhen direct (phDirectActivate abi mode) (phWhen uvm (phUVMActivate abi mode) tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -- ---- uploads, submission, completion, readback ---- def phFills = (lambda unrestricted fills : (family NvidiaPlanHostFills) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostFills (lambda unrestricted current : (family NvidiaPlanHostFills) . (family NativePhysicalCommands)) fills (branch NvidiaPlanHostFillsEnd . tail) (branch NvidiaPlanHostFillBytes host payload rest induction . (phFill host payload induction)) (branch NvidiaPlanHostFillFile host path extent rest induction . (phReadFile path host extent induction))))) def phReads = (lambda unrestricted reads : (family NvidiaPlanHostReads) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostReads (lambda unrestricted current : (family NvidiaPlanHostReads) . (family NativePhysicalCommands)) reads (branch NvidiaPlanHostReadsEnd . tail) (branch NvidiaPlanHostReadsNext host extent rest induction . (phCall phSysWrite (phArgs3 (phImm 1) (phImm host) (phImm extent)) b"" phDiscard induction))))) def nvidiaPlanHostFenceValue : Nat = 65261 def nvidiaPlanHostFenceInterval : Nat = 1000000 def nvidiaPlanHostFenceMaximumPolls : Nat = 600000 def phUSERDHost = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (phBufferHost userd)))) -- Release everything before exit: freeing the root client tears the whole -- object hierarchy down synchronously. Left to the driver's asynchronous -- reclaim at process exit, back-to-back hosts on the RTX 3090 hit -- NV_ERR_INSUFFICIENT_RESOURCES on the channel allocation about a third of -- the time, in streaks; v3 of this host, which did not free, did too. def phRelease = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy phFree (phSet32 (phZeros 16) 12 phStatusSentinel) (phCopyStateToState phFree (naturalAdd phRoot 8) 4 (phCopyStateToState (naturalAdd phFree 4) (naturalAdd phRoot 8) 4 (phCopyStateToState (naturalAdd phFree 8) (naturalAdd phRoot 8) 4 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMFree) (phState phFree)) b"" phDiscard (phCopyStateToState (phRMStatusSlot 17) (naturalAdd phFree 12) 4 (phAssertStateZero32 b"rm-free-root" (naturalAdd phFree 12) tail)))))))) -- The whole host, Strict: `submissions` is gpPut, the number of GPFIFO -- entries the plan's tables carry; `fenceHost` the host address of the -- semaphore slot the last submission releases; `statusHost`, when not 0, a -- mapped address the UVM status record is copied to before the readbacks. -- ---- native telemetry (docs/observability PRD item 9) ---- -- At each phase boundary the host appends an ALPHATEL record to -- `alpha-host.alphatel` in its working directory: the body is -- Runtime.NativeTelemetry's own encoding, made at build time (domain 1, -- event 1 "reached", the boundary's ordinal as phase and sequence, status -- 0, its name as payload), with the monotonic nanoseconds left zero; at -- run time the host reads CLOCK_MONOTONIC and Runtime.NativeTelemetrySeal -- writes the reading into the body, digests it and writes the record. A -- record exists only if the host got there, so the last one names how far -- a failed run came. The write is asserted whole (`telemetry-write`): a -- host that cannot record says so and stops, rather than running unobserved. -- Its pages: a fixed anonymous mapping of its own, taken before any device -- call, so a host with no card still records its beginning. def phTelemetryPage : Nat = 0x5E000000 def phTelemetryPadded : Nat = 0x5E000000 def phTelemetryRecord : Nat = 0x5E000400 def phTelemetryClock : Nat = 0x5E000800 def phTelemetryWork : Nat = 0x5E000C00 def phSlotTelemetry : Nat = 14 def phSlotTelemetryWritten : Nat = 15 def phTelemetryPath : Bytes = b"alpha-host.alphatel\x00" def phSysClockGettime : Nat = 228 def phClockMonotonic : Nat = 1 -- O_WRONLY | O_CREAT | O_APPEND, mode 0600 def phTelemetryOpenFlags : Nat = 1089 def phTelemetryMode : Nat = 384 def phTelemetryIdentity : Bytes = (bytes-append phIdentity (phZeros (naturalSaturatingSubtract nativeTelemetryDigestBytes (bytes-length phIdentity)))) def phTelemetryZero : (family ModelWord64) = (phWord 0) -- the body Runtime.NativeTelemetry encodes for boundary `ordinal`, its -- clock reading zero: no error code, the name as payload def phTelemetryBody = (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes . (nativeTelemetryRecordBody (phWord ordinal) phTelemetryZero (byte 1) (byte 1) (nat-to-byte ordinal) (byte 0) (constructor NativeTelemetryCounters NativeTelemetryCountersValue phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero) phTelemetryIdentity b"" name phTelemetryZero (phWord (bytes-length name))))) -- the body with SHA-256's padding: 0x80, zeros to 56 mod 64, the bit length -- (big-endian; a body is far below 8 KiB) def phTelemetryPadding = (lambda unrestricted length : Nat . (bytes-cons (byte 128) (bytes-append (phZeros (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd 55 512) length) 64)) (bytes-append (phZeros 6) (bytes-cons (nat-to-byte (naturalDivideUnchecked (naturalMultiply 8 length) 256)) (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalMultiply 8 length) 256)) b"")))))) -- map the telemetry page and put the magic in the record buffer def phTelemetryOpen = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysMmap (phArgs (phImm phTelemetryPage) (phImm 0x1000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard (phFill phTelemetryRecord b"ALPHATEL" tail))) -- boundary `ordinal`, named: seal and append its record def phTelemetry = (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted body = (phTelemetryBody ordinal name) in (let unrestricted length = (bytes-length body) in (let unrestricted padded = (bytes-append body (phTelemetryPadding length)) in (phFill phTelemetryPadded padded (phCall phSysClockGettime (phArgs3 (phImm phClockMonotonic) (phImm phTelemetryClock) (phImm 0)) b"" phDiscard (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetrySealRoutine (phArgs (phImm phTelemetryPadded) (phImm (naturalDivideUnchecked (bytes-length padded) 64)) (phImm phTelemetryRecord) (phImm length) (phImm phTelemetryClock) (phImm phTelemetryWork)) phDiscard) (phCall phSysOpenat (phArgs (phImm phAtFdCwd) phPayload (phImm phTelemetryOpenFlags) (phImm phTelemetryMode) (phImm 0) (phImm 0)) phTelemetryPath (phStore phSlotTelemetry) (phCall phSysWrite (phArgs3 (phSlot phSlotTelemetry) (phImm phTelemetryRecord) (phImm (naturalAdd 72 length))) b"" (phStore phSlotTelemetryWritten) (nativeLaunchRecipeAssertEqual (phSlot phSlotTelemetryWritten) (phImm (naturalAdd 72 length)) b"telemetry-write" (phCall phSysClose (phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0)) b"" phDiscard tail))))))))))))) -- Preparation has two ordered phases: envelope validation before any card -- call, and expansion after the buffers exist. Keeping these continuations -- here gives recipe-backed probes the same telemetry and submit/wait path -- as the ordinary host, without copying its RM command stream. def nvidiaPlanHostPreparedCommands = (lambda unrestricted before : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted mapped : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted fills : (family NvidiaPlanHostFills) . (lambda unrestricted submissions : Nat . (lambda unrestricted fenceHost : Nat . (lambda unrestricted statusHost : Nat . (lambda unrestricted reads : (family NvidiaPlanHostReads) . (phPipeCreate (phTelemetryOpen (phTelemetry 0 b"plan-host:begin" (before (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout (phTelemetry 1 b"plan-host:channel-ready" (mapped (phFills fills (phTelemetry 2 b"plan-host:uploaded" (phLoadToken (phPublish (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) submissions (phTelemetry 3 b"plan-host:submitted" (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait (phImm fenceHost) (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval)) (phTelemetry 4 b"plan-host:completed" (phWhen (naturalNonzero statusHost) (phCopyStateToMapped phUVMStatusRecord statusHost phUVMStatusRecordExtent) (phReads reads (phTelemetry 5 b"plan-host:read-back" (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess) (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))))))))))))))))))))) def phNoPreparation = (lambda unrestricted tail : (family NativePhysicalCommands) . tail) def nvidiaPlanHostCommands = (nvidiaPlanHostPreparedCommands phNoPreparation phNoPreparation) -- The channel probe, Probe mode: the prelude alone, every status after the -- root client's recorded and none asserted, then to stdout the status area -- -- the 16-byte record per buffer, the UVM slots, the RM slots -- from the -- state and the channel allocation's parameter block as the driver left it -- (its `cid` word at 132 is the hardware channel identifier), then the root -- freed. With a card it prints both and exits 0 whether or not the channel -- came up; which call refused is read off the area. def phProbeRecord : Nat = (phBufferStatus 0) def phProbeRecordExtent : Nat = (naturalSaturatingSubtract (phBufferState 0) (phBufferStatus 0)) def phChannelParamsExtent : Nat = 368 def nvidiaPlanHostProbeCommands = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (phPipeCreate (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostProbe) layout (phCall phSysWrite (phArgs3 (phImm 1) (phState phProbeRecord) (phImm phProbeRecordExtent)) b"" phDiscard (phCall phSysWrite (phArgs3 (phImm 1) (phImm phChanP) (phImm phChannelParamsExtent)) b"" phDiscard (phRelease (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess) (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))))) def phCommandCount = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . Nat) commands (branch NativePhysicalCommandsEnd . zero) (branch NativePhysicalCommandsNext head tail induction . (succ induction)))) -- The number of assertions a command list carries: what a mode decides. def phOperationIsAssert = (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . Nat) operation (branch NativePhysicalSystemCall number argv payload result . 0) (branch NativePhysicalCopyPayloadToState destination extent payload . 0) (branch NativePhysicalMachineRoutine code argv result . 0) (branch NativePhysicalFencePoll address expected polls . 0) (branch NativePhysicalTelemetryAppend path record . 0) (branch NativePhysicalAssertEqual left right error . 1) (branch NativePhysicalAssertOneOf observed first second error . 1) (branch NativePhysicalHaltSuccess . 0) (branch NativePhysicalRepeatBegin count . 0) (branch NativePhysicalRepeatEnd . 0) (branch NativePhysicalStoreWord64 destination value . 0) (branch NativePhysicalFenceWait address expected polls interval . 0) (branch NativePhysicalRepeatBeginCounted count . 0) (branch NativePhysicalAddWord64 destination left right . 0) (branch NativePhysicalFloat64 operation destination left right . 0))) def phCommandIsAssert = (lambda unrestricted command : (family NativePhysicalCommand) . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . Nat) command (branch NativePhysicalCommandValue operation identity . (phOperationIsAssert operation)))) def nvidiaPlanHostAssertionCount = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . Nat) commands (branch NativePhysicalCommandsEnd . zero) (branch NativePhysicalCommandsNext head tail induction . (naturalAdd (phCommandIsAssert head) induction)))) -- the prelude alone under a mode, for the assertion contracts def nvidiaPlanHostPreludeCommands = (lambda unrestricted mode : (family NvidiaPlanHostMode) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (phPrelude mode layout (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))) def nvidiaPlanHostProgram = (lambda unrestricted identity : Bytes . (lambda unrestricted commands : (family NativePhysicalCommands) . (constructor NativePhysicalProgram NativePhysicalProgramValue (phWord phStateExtent) (phWord phSlots) commands (phCommandCount commands) identity zero))) def nvidiaPlanHostELF = (lambda unrestricted identity : Bytes . (lambda unrestricted commands : (family NativePhysicalCommands) . (nativePhysicalGenerateNativeELFBytesDirect (nvidiaPlanHostProgram identity commands))))