1module Platform.Linux.Nvidia.PlanHost
2
3import Data.Bytes
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Compiler.MachineX86Native
9import Compiler.MachineX86NativeAssembly
10import Runtime.ArenaCertificate
11import Runtime.NativeLaunchRecipeLoad
12import Runtime.NativeTelemetry
13import Runtime.NativeTelemetrySeal
14import Runtime.NativePhysicalProgram
15import Runtime.NativePhysicalNativeELF
16import Runtime.NativePhysicalTrainingRoutine
17import Std.Natural
18
19-- The host the compiler derives from a whole-program plan: the compute-channel
20-- protocol the SM86 launch ladder proved on the RTX 3070 and the RTX 3090
21-- (rungs D..Q, Coppelius S5, the checked linear step), as typed command
22-- builders parameterised by the plan's placement. Every address, extent and
23-- handle is a parameter or derived from one; the protocol is stated once,
24-- here, for every plan.
25--
26-- Two lifecycles, selected by the layout:
27-- direct-RM every buffer is system memory; its GPU range is a fixed RM
28-- virtual reservation and a DMA map; the channel has 0x400
29-- entries and its own USERD buffer.
30-- UVM RM's VA space is duplicated into the UVM driver; buffers are
31-- external ranges mapped through it; video-memory buffers are
32-- allowed and are not host-mapped; the GPFIFO is one contiguous
33-- video allocation whose last page is USERD; the channel is
34-- registered with UVM and scheduled last. This is the
35-- lifecycle the Coppelius training executables run.
36--
37-- In order: open the card and the control node; root, device, subdevice,
38-- UVM: the DMA selector, the VA space, UVM: initialise the driver, register
39-- the GPU and the VA space, reserve the external range; the fixed buffers
40-- GPFIFO, pushbuffer, semaphores, program, QMD, direct-RM: USERD, and every
41-- data buffer; the error notifier; channel group, context share, channel,
42-- compute and usermode objects; direct-RM: bind, schedule, token, doorbell;
43-- UVM: doorbell, preemption, token, register the channel, schedule. Then
44-- the uploads, gpPut, the doorbell, a FenceWait on the plan's semaphore, the
45-- readbacks to stdout, exit 0. Every driver status is pre-set to a sentinel
46-- and recorded after the call; under NvidiaPlanHostStrict (the executables)
47-- each is asserted zero too, so a host without a card stops at its first
48-- device call with a command failure; under NvidiaPlanHostProbe (the
49-- channel probe) none after the root's is, and the host prints the status
50-- area. The root client is freed before exit.
51--
52-- Measured on the RTX 3090, driver 580.126.09, 2026-09-22, the checked
53-- linear step: UVM lifecycle 11/11 runs; two submissions per host, one
54-- semaphore slot each: 6/6, both slots released with timestamps. The
55-- direct-RM channel allocation used to fail NV_ERR_INSUFFICIENT_RESOURCES
56-- 0x1e intermittently, in streaks, at a rate that drifted with the host
57-- machine's other tenants (3/10 .. 17/60). Root-caused 2026-09-23 with the
58-- channel probe, one placement at a time interleaved with the baseline:
59-- the cause is USERD as a separate SYSTEM-memory allocation. Not the
60-- channel flags, the bind, the schedule, the root free, the work, the
61-- GPFIFO's memory or the error notifier's (each within noise of the
62-- baseline); USERD in video memory 0/60 against 17/60, and the step with
63-- USERD in video memory 60/60 records bit-identical against 6/60 failures
64-- of the old host interleaved. The Ampere direct-RM profile therefore admits
65-- a layout only with a video-memory USERD (nvidiaPlanHostLayoutAdmitted);
66-- the UVM lifecycle's USERD is the last page of its video GPFIFO already.
67
68-- System memory is one physically contiguous allocation; paged system
69-- memory is not (NVOS32 PHYSICALITY NONCONTIGUOUS), which is what a buffer
70-- too large for contiguous pages needs -- the GB10's arena, which has no
71-- video memory to live in. The GPU reaches either through its page tables.
72family NvidiaPlanHostMemory : Type 0
73constructor NvidiaPlanHostSystemMemory
74constructor NvidiaPlanHostVideoMemory
75-- Noncontiguous physical pages, still host-cached and GPU virtually contiguous.
76constructor NvidiaPlanHostPagedSystemMemory
77-- Noncontiguous system memory the GPU caches in its L2, in 64 KiB pages,
78-- never mapped into the process: the allocation cudaMalloc makes on the GB10
79-- (read off the driver's RM calls, 2026-09-26: NV01_MEMORY_SYSTEM, attr
80-- PAGE_SIZE_BIG | LOCATION_PCI | PHYSICALITY_NONCONTIGUOUS, attr2
81-- GPU_CACHEABLE_YES | ZBC_PREFER_NO_ZBC, flags IGNORE_BANK_PLACEMENT |
82-- MEMORY_HANDLE_PROVIDED | MAP_NOT_REQUIRED, PTE kind 6, 64 KiB aligned).
83-- Paged system memory is not L2-cached by the GPU: an L2-resident copy runs
84-- at 190 GB/s there against 880 GB/s here.
85constructor NvidiaPlanHostGPUCachedSystemMemory
86end-family
87
88-- host 0 = not mapped into the process
89family NvidiaPlanHostBuffer : Type 0
90constructor NvidiaPlanHostBufferValue
91field unrestricted nvidiaPlanHostBufferIdentity : Bytes
92field unrestricted nvidiaPlanHostBufferGPU : Nat
93field unrestricted nvidiaPlanHostBufferHost : Nat
94field unrestricted nvidiaPlanHostBufferExtent : Nat
95field unrestricted nvidiaPlanHostBufferMemory : (family NvidiaPlanHostMemory)
96end-family
97
98family NvidiaPlanHostBuffers : Type 0
99constructor NvidiaPlanHostBuffersEnd
100constructor NvidiaPlanHostBuffersNext
101field unrestricted nvidiaPlanHostBuffersHead : (family NvidiaPlanHostBuffer)
102recursive unrestricted nvidiaPlanHostBuffersTail
103end-family
104
105family NvidiaPlanHostABI : Type 0
106constructor NvidiaPlanHostABIValue
107field unrestricted nvidiaPlanHostMapDMAIoctl : Nat
108field unrestricted nvidiaPlanHostNVOS46Size : Nat
109field unrestricted nvidiaPlanHostNVOS46DMAOffset : Nat
110field unrestricted nvidiaPlanHostNVOS46Status : Nat
111field unrestricted nvidiaPlanHostChannelClass : Nat
112field unrestricted nvidiaPlanHostComputeClass : Nat
113field unrestricted nvidiaPlanHostUsermodeClass : Nat
114field unrestricted nvidiaPlanHostEngineType : Nat
115-- the first four bytes of the driver version the ABI was built for,
116-- little-endian ("580." is 0x2E303835): the host asks the driver for its
117-- version before any card call and refuses another branch by name
118field unrestricted nvidiaPlanHostDriverBranch : Nat
119-- the bytes of NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS: 2 on the 570 branch
120-- (bEnable, bSkipSubmit), 3 from 580 (bSkipEnable added); the wrong size is
121-- NV_ERR_INVALID_ARGUMENT (0x1f), measured on an RTX A6000, 570.195.03
122field unrestricted nvidiaPlanHostScheduleParamsSize : Nat
123-- Required location of a separately allocated direct-RM USERD buffer.
124-- Discrete Ampere needs video memory; the measured integrated GB10 path
125-- uses system memory. This is target policy, not a runtime retry choice.
126field unrestricted nvidiaPlanHostDirectUSERDMemory : (family NvidiaPlanHostMemory)
127field unrestricted nvidiaPlanHostDirectChannelFlags : Nat
128-- Direct-RM cache snooping is target policy. The GB10 bring-up's host-cached
129-- system buffers use 0x8010; the qualified Ampere path keeps 0x8000. See
130-- Memory.ABI.memoryABIDMAMappingFlags. A CPU publication barrier alone does
131-- not make a non-snooping GPU mapping coherent with cached CPU writes.
132field unrestricted nvidiaPlanHostDirectDMAFlags : Nat
133end-family
134
135-- one upload: bytes, or the contents of a file at run time
136family NvidiaPlanHostFills : Type 0
137constructor NvidiaPlanHostFillsEnd
138constructor NvidiaPlanHostFillBytes
139field unrestricted nvidiaPlanHostFillHost : Nat
140field unrestricted nvidiaPlanHostFillPayload : Bytes
141recursive unrestricted nvidiaPlanHostFillsTail
142constructor NvidiaPlanHostFillFile
143field unrestricted nvidiaPlanHostFillFileHost : Nat
144field unrestricted nvidiaPlanHostFillFilePath : Bytes
145field unrestricted nvidiaPlanHostFillFileExtent : Nat
146recursive unrestricted nvidiaPlanHostFillFileTail
147end-family
148
149-- one readback: a host range written to stdout after completion
150family NvidiaPlanHostReads : Type 0
151constructor NvidiaPlanHostReadsEnd
152constructor NvidiaPlanHostReadsNext
153field unrestricted nvidiaPlanHostReadHost : Nat
154field unrestricted nvidiaPlanHostReadExtent : Nat
155recursive unrestricted nvidiaPlanHostReadsTail
156end-family
157
158family NvidiaPlanHostLifecycle : Type 0
159constructor NvidiaPlanHostDirectRM
160constructor NvidiaPlanHostUVM
161field unrestricted nvidiaPlanHostExternalRangeBase : Nat
162field unrestricted nvidiaPlanHostExternalRangeExtent : Nat
163end-family
164
165-- How the host treats a driver status. Strict: every one is asserted zero
166-- (the executables). Probe: every one after the root client's is recorded
167-- and none asserted, so a host on a card reports which call refused instead
168-- of stopping at it (the channel probe). The card-name and driver-branch
169-- assertions hold in both: a probe against the wrong card, or a driver
170-- whose ABI the host was not built for, stops.
171family NvidiaPlanHostMode : Type 0
172constructor NvidiaPlanHostStrict
173constructor NvidiaPlanHostProbe
174end-family
175
176family NvidiaPlanHostLayout : Type 0
177constructor NvidiaPlanHostLayoutValue
178field unrestricted nvidiaPlanHostGPFIFO : (family NvidiaPlanHostBuffer)
179field unrestricted nvidiaPlanHostPushbuffer : (family NvidiaPlanHostBuffer)
180field unrestricted nvidiaPlanHostSemaphores : (family NvidiaPlanHostBuffer)
181field unrestricted nvidiaPlanHostProgram : (family NvidiaPlanHostBuffer)
182field unrestricted nvidiaPlanHostQMD : (family NvidiaPlanHostBuffer)
183field unrestricted nvidiaPlanHostUSERD : (family NvidiaPlanHostBuffer)
184field unrestricted nvidiaPlanHostData : (family NvidiaPlanHostBuffers)
185field unrestricted nvidiaPlanHostABI : (family NvidiaPlanHostABI)
186field unrestricted nvidiaPlanHostLifecycle : (family NvidiaPlanHostLifecycle)
187field unrestricted nvidiaPlanHostExpectedName : Bytes
188-- the host address the error notifier page is mapped at, 0 = not mapped
189field unrestricted nvidiaPlanHostErrorHost : Nat
190end-family
191
192-- The 570 branch: the 56-byte NVOS46 (the layout the retired 575 ABI of
193-- the RTX 3070 fixtures used) and the 2-byte schedule parameters. The 575
194-- branch is no longer offered for any sm_86 card on RunPod (2026-09-24:
195-- 570.195, 580.65 .. 580.178, 595.91), so its ABI could not be qualified
196-- again and was retired; this one is qualified on an RTX A6000, 570.195.03.
197def nvidiaPlanHostAmpere570 : (family NvidiaPlanHostABI) =
198 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0384657 56 40 48 0xC56F 0xC7C0 0xC561 0 0x2E303735 2
199 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000)
200
201def nvidiaPlanHostAmpere580 : (family NvidiaPlanHostABI) =
202 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC56F 0xC7C0 0xC561 0 0x2E303835 3
203 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000)
204
205-- The DGX Spark's GB10 (compute 12.1) on the 580 branch: the 580 DMA-map ABI
206-- above with the classes this GPU's class list offers and the ladder
207-- allocated (tools/dgx/rung_tsg.py, rung_execute.py): BLACKWELL_CHANNEL_GPFIFO_A
208-- 0xC96F, BLACKWELL_COMPUTE_B 0xCEC0, HOPPER_USERMODE_A 0xC661.
209def nvidiaPlanHostBlackwell580 : (family NvidiaPlanHostABI) =
210 (constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC96F 0xCEC0 0xC661 0 0x2E303835 3
211 -- USERD in system memory (the GB10's channel buffers, Coppelius.Build.
212 -- NativeHost), the channel flags every UVM plan allocates with, and the
213 -- direct-RM DMA flags, which a UVM plan never reads
214 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory) 0x01000000 0x8000)
215
216-- A layout built for another driver ABI: every buffer, the lifecycle and
217-- the expected card unchanged, only the ABI (the DMA-map parameters, the
218-- classes, the driver branch it demands) replaced.
219def nvidiaPlanHostWithABI =
220 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
221 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
222 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostLayout)) layout
223 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data previous lifecycle expectedName errorHost .
224 (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost)))))
225
226-- ---- operands and commands ----
227def phWord = (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))
228def phImm = nativeLaunchRecipeImmediate
229def phSlot = nativeLaunchRecipeSlotValue
230def phStore = nativeLaunchRecipeStore
231def phDiscard : (family NativePhysicalResultBinding) = (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)
232def phState = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (phWord offset)))
233def phLoad = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateLoad64 (phWord offset)))
234def phPayload : (family NativePhysicalOperand) = (constructor NativePhysicalOperand NativePhysicalPayloadAddress modelWord64Zero)
235
236def phArgs =
237 (lambda unrestricted a0 : (family NativePhysicalOperand) .
238 (lambda unrestricted a1 : (family NativePhysicalOperand) .
239 (lambda unrestricted a2 : (family NativePhysicalOperand) .
240 (lambda unrestricted a3 : (family NativePhysicalOperand) .
241 (lambda unrestricted a4 : (family NativePhysicalOperand) .
242 (lambda unrestricted a5 : (family NativePhysicalOperand) .
243 (constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5)))))))
244
245def phArgs3 =
246 (lambda unrestricted a0 : (family NativePhysicalOperand) .
247 (lambda unrestricted a1 : (family NativePhysicalOperand) .
248 (lambda unrestricted a2 : (family NativePhysicalOperand) .
249 (phArgs a0 a1 a2 (phImm 0) (phImm 0) (phImm 0)))))
250
251def phIdentity : Bytes = b"nvidia-plan-host"
252
253def phNext =
254 (lambda unrestricted operation : (family NativePhysicalOperation) .
255 (lambda unrestricted tail : (family NativePhysicalCommands) .
256 (nativeLaunchRecipeCommand operation phIdentity tail)))
257
258def phCall =
259 (lambda unrestricted number : Nat .
260 (lambda unrestricted argv : (family NativePhysicalArguments) .
261 (lambda unrestricted payload : Bytes .
262 (lambda unrestricted result : (family NativePhysicalResultBinding) .
263 (lambda unrestricted tail : (family NativePhysicalCommands) .
264 (phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phImm number) argv payload result) tail))))))
265
266def phCopy =
267 (lambda unrestricted offset : Nat .
268 (lambda unrestricted payload : Bytes .
269 (lambda unrestricted tail : (family NativePhysicalCommands) .
270 (phNext (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (phWord offset) (phWord (bytes-length payload)) payload) tail))))
271
272-- Linux x86-64
273def phSysRead : Nat = 0
274def phSysWrite : Nat = 1
275def phSysClose : Nat = 3
276def phSysMmap : Nat = 9
277def phSysIoctl : Nat = 16
278def phSysDup2 : Nat = 33
279def phSysExitGroup : Nat = 231
280def phSysOpenat : Nat = 257
281def phSysPipe2 : Nat = 293
282def phAtFdCwd : Nat = 18446744073709551516
283def phOpenFlags : Nat = 0x80002
284def phMapAnonymousFixed : Nat = 0x32
285def phMapSharedFixed : Nat = 0x11
286def phNoDescriptor : Nat = 18446744073709551615
287
288-- RM and UVM escapes
289def phRMAlloc : Nat = 0xC020462B
290def phRMControl : Nat = 0xC020462A
291def phRMMapMemory : Nat = 0xC038464E
292def phRMFree : Nat = 0xC0104629
293def phRegisterFD : Nat = 0xC00446C9
294def phWaitOpen : Nat = 0xC00846DA
295def phUVMInitialize : Nat = 0x30000001
296def phUVMMMInitialize : Nat = 75
297def phUVMRegisterGPU : Nat = 37
298def phUVMRegisterGPUVASpace : Nat = 25
299def phUVMRegisterChannel : Nat = 27
300def phUVMCreateExternalRange : Nat = 73
301def phUVMMapExternalAllocation : Nat = 33
302def phUVMChannelRangeBase : Nat = 0xA00000000
303def phUVMChannelRangeExtent : Nat = 0x4000000
304
305-- result slots and fixed descriptors
306def phSlotControl : Nat = 0
307def phSlotGPU : Nat = 1
308def phSlotMap : Nat = 2
309def phSlotFile : Nat = 3
310-- slots 4..13 belong to the request host (PlanHostRequest), 14 and 15 to
311-- the native telemetry. Transfers own the next slot and never overwrite a
312-- request file descriptor or a mapping result while checking short I/O.
313def phSlotTransfer : Nat = 16
314def phSlots : Nat = (succ phSlotTransfer)
315def phFdControl : Nat = 100
316def phFdCard : Nat = 101
317def phFdMap : Nat = 102
318def phFdUVM : Nat = 103
319def phFdUVMMemoryMap : Nat = 104
320
321-- RM handles, caller-chosen for children
322def phHDevice : Nat = 0xDEAD0080
323def phHSubdevice : Nat = 0xDEAD2080
324def phHVASpace : Nat = 0xDEAD90F1
325def phHError : Nat = 0xDEAD0E44
326def phHGroup : Nat = 0xDEADA06C
327def phHContext : Nat = 0xDEAD9067
328def phHDMA : Nat = 0xDEAD0070
329def phHMemory = (lambda unrestricted index : Nat . (naturalAdd 0xB0000000 index))
330def phHVirtual = (lambda unrestricted index : Nat . (naturalAdd 0xB1000000 index))
331def phHClass = (lambda unrestricted class : Nat . (naturalAdd 0xDEAD0000 class))
332
333-- state layout, 16 KiB: RM call blocks, then a 16-byte status record per
334-- buffer, then 256 bytes of call blocks per buffer (at most 24 buffers, to
335-- 10240); the request host's areas follow (PlanHostRequest)
336def phStateExtent : Nat = 16384
337def phBufferBlocksEnd : Nat = 10240
338def phRoot : Nat = 0
339def phDev : Nat = 64
340def phSub : Nat = 128
341def phVAS : Nat = 192
342def phErrMap : Nat = 256
343def phErr : Nat = 2048
344def phGroup : Nat = 2112
345def phCtx : Nat = 2176
346def phChan : Nat = 2240
347def phComp : Nat = 2304
348def phUser : Nat = 2368
349def phBind : Nat = 2432
350def phSched : Nat = 2496
351def phTok : Nat = 2560
352def phDoorMap : Nat = 2624
353def phWait : Nat = 2688
354def phPipe : Nat = 2752
355def phScratch : Nat = 2816
356def phName : Nat = 2880
357def phPreempt : Nat = 3008
358def phFree : Nat = 3040
359def phDMAObject : Nat = 3072
360def phUVMControl : Nat = 3136
361def phBufferState = (lambda unrestricted index : Nat . (naturalAdd 4096 (naturalMultiply index 256)))
362def phBufferStatus = (lambda unrestricted index : Nat . (naturalAdd 3200 (naturalMultiply index 16)))
363def phBuffersMaximum : Nat = 24
364
365-- the fixed anonymous parameter page, 64 KiB
366def phParams : Nat = 0x50000000
367def phDevP : Nat = 0x50000000
368def phSubP : Nat = 0x50000100
369def phVASP : Nat = 0x50000200
370def phErrP : Nat = 0x50001100
371def phGroupP : Nat = 0x50001200
372def phCtxP : Nat = 0x50001300
373def phChanP : Nat = 0x50001400
374def phBindP : Nat = 0x50001600
375def phSchedP : Nat = 0x50001700
376def phTokP : Nat = 0x50001800
377def phRegFdP : Nat = 0x50001980
378def phPreemptP : Nat = 0x50001A00
379def phNameP : Nat = 0x50001B00
380def phMemP = (lambda unrestricted index : Nat . (naturalAdd 0x50002000 (naturalMultiply index 0x200)))
381def phVirtP = (lambda unrestricted index : Nat . (naturalAdd 0x50002100 (naturalMultiply index 0x200)))
382def phDMAObjectP : Nat = 0x50007F00
383def phUVMGidP : Nat = 0x50008000
384def phUVMInitP : Nat = 0x50008200
385def phUVMMMP : Nat = 0x50008300
386def phUVMRegisterGPUP : Nat = 0x50008400
387def phUVMRegisterVASpaceP : Nat = 0x50008500
388def phUVMRegisterChannelP : Nat = 0x50008600
389def phUVMCreateRangeP : Nat = 0x50008700
390def phUVMMapAllocationP : Nat = 0x50009000
391def phDoorHost : Nat = 0x60800000
392def phStatusSentinel : Nat = 0xFFFFFFFF
393
394-- ---- little-endian blocks ----
395def phZeros =
396 (lambda unrestricted count : Nat .
397 (nat-eliminate
398 (lambda unrestricted current : Nat . Bytes)
399 b""
400 (lambda unrestricted predecessor : Nat .
401 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
402 count))
403
404def phDrop = dataBytesDropValidated
405
406def phTake = dataBytesTakeValidated
407
408def phW32 = (lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value)))
409def phW64 = (lambda unrestricted value : Nat . (dataBytesWord64LE (phWord value)))
410
411def phSet =
412 (lambda unrestricted block : Bytes .
413 (lambda unrestricted offset : Nat .
414 (lambda unrestricted field : Bytes .
415 (bytes-append (phTake offset block) (bytes-append field (phDrop (naturalAdd offset (bytes-length field)) block))))))
416
417def phSet32 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW32 value)))))
418def phSet64 = (lambda unrestricted block : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted value : Nat . (phSet block offset (phW64 value)))))
419
420-- ---- the pipe memcpy ----
421def phCopyStateToState =
422 (lambda unrestricted destination : Nat .
423 (lambda unrestricted source : Nat .
424 (lambda unrestricted count : Nat .
425 (lambda unrestricted tail : (family NativePhysicalCommands) .
426 (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) (phState source) (phImm count)) b"" phDiscard
427 (phCall phSysRead (phArgs3 (phLoad phPipe) (phState destination) (phImm count)) b"" phDiscard tail))))))
428
429-- A pipe is not an unbounded staging buffer. A single-threaded write/read
430-- pair deadlocks when its write exceeds capacity (the matrix qualification
431-- stopped in write(901120), after filling 65536 bytes). Drain every bounded
432-- chunk before writing another. Linux PIPE_BUF is 4096 on both target ABIs;
433-- the empty pipe admits that atomic extent even when capacity is one page.
434-- Short/error returns fail by name, including interruption; no partial copy
435-- is reported as a successful upload. Result slot ownership is explicit.
436def phPipeChunkBytes : Nat = 4096
437def phPipeChunkCount = (lambda unrestricted count : Nat .
438 (naturalAdd (naturalDivideUnchecked count phPipeChunkBytes)
439 (naturalNonzero (naturalModuloUnchecked count phPipeChunkBytes))))
440def phPipeChunk = (lambda unrestricted source : (family NativePhysicalOperand) .
441 (lambda unrestricted destination : (family NativePhysicalOperand) .
442 (lambda unrestricted count : Nat . (lambda unrestricted payload : Bytes .
443 (lambda unrestricted tail : (family NativePhysicalCommands) .
444 (phCall phSysWrite (phArgs3 (phLoad (naturalAdd phPipe 4)) source (phImm count)) payload (phStore phSlotTransfer)
445 (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-write"
446 (phCall phSysRead (phArgs3 (phLoad phPipe) destination (phImm count)) b"" (phStore phSlotTransfer)
447 (nativeLaunchRecipeAssertEqual (phSlot phSlotTransfer) (phImm count) b"pipe-copy-read" tail)))))))))
448def phFill = (lambda unrestricted address : Nat . (lambda unrestricted payload : Bytes .
449 (lambda unrestricted tail : (family NativePhysicalCommands) .
450 (app (nat-eliminate
451 (lambda unrestricted remaining : Nat .
452 (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))))
453 (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . tail))
454 (lambda unrestricted predecessor : Nat .
455 (lambda unrestricted induction : (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))) .
456 (lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes .
457 (let unrestricted count = (naturalMinimum phPipeChunkBytes (bytes-length bytes)) in
458 (phPipeChunk phPayload (phImm at) count (dataBytesTakeValidated count bytes)
459 (induction (naturalAdd at count) (dataBytesDropValidated count bytes))))))))
460 (phPipeChunkCount (bytes-length payload))) address payload))))
461-- Address-based copies share the same transfer/check mechanism. Their
462-- ranges must be disjoint as before; this is not an overlapping memmove.
463def phPipeRanges = (lambda unrestricted source : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
464 (lambda unrestricted destination : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
465 (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) .
466 (let unrestricted chunks = (phPipeChunkCount count) in
467 (nat-eliminate (lambda unrestricted i : Nat . (family NativePhysicalCommands)) tail
468 (lambda unrestricted index : Nat . (lambda unrestricted rest : (family NativePhysicalCommands) .
469 (let unrestricted offset = (naturalMultiply (naturalSaturatingSubtract chunks (succ index)) phPipeChunkBytes) in
470 (phPipeChunk (source offset) (destination offset)
471 (naturalMinimum phPipeChunkBytes (naturalSaturatingSubtract count offset)) b"" rest)))) chunks))))))
472def phCopyMappedToState = (lambda unrestricted address : Nat . (lambda unrestricted destination : Nat .
473 (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset)))
474 (lambda unrestricted offset : Nat . (phState (naturalAdd destination offset))))))
475def phCopyStateToMapped = (lambda unrestricted source : Nat . (lambda unrestricted address : Nat .
476 (phPipeRanges (lambda unrestricted offset : Nat . (phState (naturalAdd source offset)))
477 (lambda unrestricted offset : Nat . (phImm (naturalAdd address offset))))))
478def phCopyMappedToMapped = (lambda unrestricted source : Nat . (lambda unrestricted destination : Nat .
479 (phPipeRanges (lambda unrestricted offset : Nat . (phImm (naturalAdd source offset)))
480 (lambda unrestricted offset : Nat . (phImm (naturalAdd destination offset))))))
481
482-- the pipe the memcpys above go through; every entry point creates it first
483def phPipeCreate =
484 (lambda unrestricted tail : (family NativePhysicalCommands) .
485 (phCall phSysPipe2 (phArgs3 (phState phPipe) (phImm 0) (phImm 0)) b"" phDiscard tail))
486
487-- Read the declared prefix into a mapped buffer. Short reads (including
488-- interruption), missing files and I/O errors fail before later uploads or
489-- submissions; an unread suffix is allowed by this fill's prefix contract.
490-- Keep the descriptor in phScratch while phSlotFile carries read/close
491-- results. Both are owned temporaries across this straight-line fragment;
492-- no caller's request or telemetry slot is borrowed. Closing also prevents
493-- a multi-tensor import from exhausting the process's file descriptors.
494-- Bytes has an explicit extent; openat requires a terminating zero. An
495-- eight-byte path otherwise runs into the next payload in the host image.
496-- Caller-supplied trailing zeros remain harmless; never rely on pool padding.
497def phReadFile =
498 (lambda unrestricted path : Bytes .
499 (lambda unrestricted address : Nat .
500 (lambda unrestricted count : Nat .
501 (lambda unrestricted tail : (family NativePhysicalCommands) .
502 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm 0)) (bytes-append path b"\x00") (phStore phSlotFile)
503 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState phScratch) (phSlot phSlotFile))
504 (phCall phSysRead (phArgs3 (phSlot phSlotFile) (phImm address) (phImm count)) b"" (phStore phSlotFile)
505 (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm count) b"input-file-read"
506 (phCall phSysClose (phArgs3 (phLoad phScratch) (phImm 0) (phImm 0)) b"" (phStore phSlotFile)
507 (nativeLaunchRecipeAssertEqual (phSlot phSlotFile) (phImm 0) b"input-file-close" tail))))))))))
508
509def phRangeBase =
510 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
511 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
512 (branch NvidiaPlanHostDirectRM . 0)
513 (branch NvidiaPlanHostUVM base extent . base)))
514
515def phRangeExtent =
516 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
517 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
518 (branch NvidiaPlanHostDirectRM . 0)
519 (branch NvidiaPlanHostUVM base extent . extent)))
520
521-- 1 when the buffer lies inside the lifecycle's pre-created external range,
522-- the video arena: such a buffer is mapped into the range, not given one
523def phInsideRange =
524 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
525 (lambda unrestricted gpu : Nat .
526 (lambda unrestricted extent : Nat .
527 (naturalAnd (naturalNonzero (phRangeExtent lifecycle))
528 (naturalAnd (naturalLessOrEqual (phRangeBase lifecycle) gpu)
529 (naturalLessOrEqual (naturalAdd gpu extent) (naturalAdd (phRangeBase lifecycle) (phRangeExtent lifecycle))))))))
530
531def phWhen =
532 (lambda unrestricted flag : Nat .
533 (lambda unrestricted commands : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
534 (lambda unrestricted tail : (family NativePhysicalCommands) .
535 (nat-eliminate
536 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
537 tail
538 (lambda unrestricted predecessor : Nat .
539 (lambda unrestricted ignored : (family NativePhysicalCommands) . (commands tail)))
540 flag))))
541
542-- ---- fail closed ----
543def phAssertStateZero32 =
544 (lambda unrestricted identity : Bytes .
545 (lambda unrestricted offset : Nat .
546 (lambda unrestricted tail : (family NativePhysicalCommands) .
547 (phCopy phScratch (phZeros 8)
548 (phCopyStateToState phScratch offset 4
549 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
550
551def phAssertMappedZero32 =
552 (lambda unrestricted identity : Bytes .
553 (lambda unrestricted address : Nat .
554 (lambda unrestricted tail : (family NativePhysicalCommands) .
555 (phCopy phScratch (phZeros 8)
556 (phCopyMappedToState address phScratch 4
557 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
558
559-- the same, unless tolerated
560def phCheckStateZero32 =
561 (lambda unrestricted identity : Bytes .
562 (lambda unrestricted tolerate : Nat .
563 (lambda unrestricted offset : Nat .
564 (lambda unrestricted tail : (family NativePhysicalCommands) .
565 (phWhen (naturalIsZero tolerate) (phAssertStateZero32 identity offset) tail)))))
566
567def phCheckMappedZero32 =
568 (lambda unrestricted identity : Bytes .
569 (lambda unrestricted tolerate : Nat .
570 (lambda unrestricted address : Nat .
571 (lambda unrestricted tail : (family NativePhysicalCommands) .
572 (phWhen (naturalIsZero tolerate) (phAssertMappedZero32 identity address) tail)))))
573
574-- ---- RM alloc / control, each asserted ----
575def phAlloc =
576 (lambda unrestricted identity : Bytes .
577 (lambda unrestricted tolerate : Nat .
578 (lambda unrestricted block : Nat .
579 (lambda unrestricted parent : Nat .
580 (lambda unrestricted class : Nat .
581 (lambda unrestricted paramsAddress : Nat .
582 (lambda unrestricted paramsSize : Nat .
583 (lambda unrestricted handle : Nat .
584 (lambda unrestricted statusOffset : Nat .
585 (lambda unrestricted tail : (family NativePhysicalCommands) .
586 (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 parent) 8 handle) 12 class) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel)
587 (phCopyStateToState block (naturalAdd phRoot 8) 4
588 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState block)) b"" phDiscard
589 (phCopyStateToState statusOffset (naturalAdd block 28) 4
590 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail)))))))))))))))
591
592def phControl =
593 (lambda unrestricted identity : Bytes .
594 (lambda unrestricted tolerate : Nat .
595 (lambda unrestricted statusOffset : Nat .
596 (lambda unrestricted block : Nat .
597 (lambda unrestricted object : Nat .
598 (lambda unrestricted command : Nat .
599 (lambda unrestricted paramsAddress : Nat .
600 (lambda unrestricted paramsSize : Nat .
601 (lambda unrestricted tail : (family NativePhysicalCommands) .
602 (phCopy block (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 4 object) 8 command) 16 paramsAddress) 24 paramsSize) 28 phStatusSentinel)
603 (phCopyStateToState block (naturalAdd phRoot 8) 4
604 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMControl) (phState block)) b"" phDiscard
605 (phCopyStateToState statusOffset (naturalAdd block 28) 4
606 (phCheckStateZero32 identity tolerate (naturalAdd block 28) tail))))))))))))))
607
608-- a UVM ioctl whose status word lives in its parameter block: the word is
609-- recorded in the UVM status record, one 4-byte slot per call, and asserted
610-- zero unless the call is one the proven hosts tolerate a non-zero from
611def phUVMStatusRecord : Nat = 3584
612def phUVMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd phUVMStatusRecord (naturalMultiply slot 4)))
613def phUVMStatusRecordExtent : Nat = 512
614 -- RM status record slots after the UVM slots
615def phRMStatusSlot = (lambda unrestricted slot : Nat . (naturalAdd 4000 (naturalMultiply slot 4)))
616
617-- the `tolerate` an RM alloc or control takes under a mode
618def phTolerate =
619 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
620 (eliminate NvidiaPlanHostMode (lambda unrestricted current : (family NvidiaPlanHostMode) . Nat) mode
621 (branch NvidiaPlanHostStrict . 0)
622 (branch NvidiaPlanHostProbe . 1)))
623
624def phUVMCall =
625 (lambda unrestricted identity : Bytes .
626 (lambda unrestricted slot : Nat .
627 (lambda unrestricted tolerate : Nat .
628 (lambda unrestricted descriptor : Nat .
629 (lambda unrestricted request : Nat .
630 (lambda unrestricted paramsAddress : Nat .
631 (lambda unrestricted statusOffset : Nat .
632 (lambda unrestricted tail : (family NativePhysicalCommands) .
633 (phCall phSysIoctl (phArgs3 (phImm descriptor) (phImm request) (phImm paramsAddress)) b"" phDiscard
634 (phCopyMappedToState (naturalAdd paramsAddress statusOffset) (phUVMStatusSlot slot) 4
635 (phCheckMappedZero32 identity tolerate (naturalAdd paramsAddress statusOffset) tail)))))))))))
636
637-- the same, right after the UVM device was opened onto `descriptor`: the
638-- dup2 that placed it returned `descriptor` (it returns a negative errno
639-- when the open failed), or -- unless `openTolerate` -- the host stops with
640-- `uvm-open`, not at the ioctl that finds no device behind the descriptor.
641-- Measured on RunPod, 2026-09-24: a container whose /dev/nvidia-uvm exists
642-- but opens with EIO used to stop at `uvm-initialize`.
643def phUVMCallAfterOpen =
644 (lambda unrestricted openTolerate : Nat .
645 (lambda unrestricted identity : Bytes .
646 (lambda unrestricted slot : Nat .
647 (lambda unrestricted tolerate : Nat .
648 (lambda unrestricted descriptor : Nat .
649 (lambda unrestricted request : Nat .
650 (lambda unrestricted paramsAddress : Nat .
651 (lambda unrestricted statusOffset : Nat .
652 (lambda unrestricted tail : (family NativePhysicalCommands) .
653 (phWhen (naturalIsZero openTolerate)
654 (nativeLaunchRecipeAssertEqual (phSlot phSlotMap) (phImm descriptor) b"uvm-open")
655 (phUVMCall identity slot tolerate descriptor request paramsAddress statusOffset tail)))))))))))
656
657-- ---- buffers ----
658def phBufferGPU =
659 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
660 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
661 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . gpu)))
662def phBufferHost =
663 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
664 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
665 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . host)))
666def phBufferExtent =
667 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
668 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
669 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . extent)))
670def phBufferIsVideo =
671 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
672 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
673 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
674 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
675 (branch NvidiaPlanHostSystemMemory . 0)
676 (branch NvidiaPlanHostVideoMemory . 1)
677 (branch NvidiaPlanHostPagedSystemMemory . 0)
678 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
679
680def phBufferIsPaged =
681 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
682 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
683 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
684 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
685 (branch NvidiaPlanHostSystemMemory . 0)
686 (branch NvidiaPlanHostVideoMemory . 0)
687 (branch NvidiaPlanHostPagedSystemMemory . 1)
688 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
689
690def phBufferIsGPUCached =
691 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
692 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) buffer
693 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
694 (eliminate NvidiaPlanHostMemory (lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat) memory
695 (branch NvidiaPlanHostSystemMemory . 0)
696 (branch NvidiaPlanHostVideoMemory . 0)
697 (branch NvidiaPlanHostPagedSystemMemory . 0)
698 (branch NvidiaPlanHostGPUCachedSystemMemory . 1)))))
699
700def phABI =
701 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
702 (lambda unrestricted which : Nat .
703 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
704 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags .
705 (naturalSelect (naturalEqual which 0) mapDMA
706 (naturalSelect (naturalEqual which 1) size
707 (naturalSelect (naturalEqual which 2) dmaOffset
708 (naturalSelect (naturalEqual which 3) status
709 (naturalSelect (naturalEqual which 4) channel
710 (naturalSelect (naturalEqual which 5) compute
711 (naturalSelect (naturalEqual which 6) usermode (naturalSelect (naturalEqual which 7) engine (naturalSelect (naturalEqual which 8) driverBranch
712 (naturalSelect (naturalEqual which 9) scheduleSize channelFlags))))))))))))))
713
714def phUSERDRequiresVideo =
715 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
716 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
717 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags .
718 (eliminate NvidiaPlanHostMemory (lambda unrestricted memory : (family NvidiaPlanHostMemory) . Nat) userdMemory
719 (branch NvidiaPlanHostSystemMemory . 0)
720 (branch NvidiaPlanHostVideoMemory . 1)
721 (branch NvidiaPlanHostPagedSystemMemory . 0)
722 (branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
723
724def phIsUVM =
725 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
726 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat) lifecycle
727 (branch NvidiaPlanHostDirectRM . 0)
728 (branch NvidiaPlanHostUVM base extent . 1)))
729
730-- a buffer extent for a table: the table's bytes rounded up to a unit
731def nvidiaPlanHostRoundUp =
732 (lambda unrestricted value : Nat .
733 (lambda unrestricted unit : Nat .
734 (naturalMultiply (naturalDivideUnchecked (naturalAdd value (naturalSaturatingSubtract unit 1)) unit) unit)))
735
736-- Where the host may write: the host-mapped buffers of a layout (host 0 =
737-- not mapped), the error notifier's page among them. A range is admitted
738-- when mapped buffers cover it end to end -- adjacent mappings may carry
739-- one table across their seam (Coppelius's QMD primary and overflow).
740def nvidiaPlanHostErrorPageBytes : Nat = 0x1000
741
742def phMapped =
743 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
744 (lambda unrestricted rest : (family NvidiaPlanHostBuffers) .
745 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext buffer rest)))
746
747def phLayoutMappings =
748 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
749 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout
750 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
751 (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd (phMapped userd
752 (phMapped (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue b"error-notifier" 0 errorHost nvidiaPlanHostErrorPageBytes
753 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory))
754 data))))))))))
755
756def phMappingCount =
757 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
758 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
759 (branch NvidiaPlanHostBuffersEnd . 0)
760 (branch NvidiaPlanHostBuffersNext head rest induction . (succ induction))))
761
762-- the end of the first host-mapped buffer holding the byte at `host`, 0 when none does
763def phMappingEndAt =
764 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
765 (lambda unrestricted host : Nat .
766 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
767 (branch NvidiaPlanHostBuffersEnd . 0)
768 (branch NvidiaPlanHostBuffersNext head rest induction .
769 (naturalSelect
770 (naturalAnd (naturalNonzero (phBufferHost head))
771 (naturalAnd (naturalLessOrEqual (phBufferHost head) host)
772 (naturalLess host (naturalAdd (phBufferHost head) (phBufferExtent head)))))
773 (naturalAdd (phBufferHost head) (phBufferExtent head))
774 induction)))))
775
776-- 1 when the buffers cover [host, host + extent): step from mapping to
777-- mapping, at most once per mapping (the fuel)
778def phCovers =
779 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
780 (lambda unrestricted fuel : Nat .
781 (nat-eliminate
782 (lambda unrestricted current : Nat . (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)))
783 (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (naturalEqual extent 0)))
784 (lambda unrestricted predecessor : Nat .
785 (lambda unrestricted induction : (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)) .
786 (lambda unrestricted host : Nat .
787 (lambda unrestricted extent : Nat .
788 (let unrestricted end = (phMappingEndAt buffers host)
789 in (naturalSelect (naturalEqual extent 0) 1
790 (naturalSelect (naturalEqual end 0) 0
791 (induction end (naturalSaturatingSubtract (naturalAdd host extent) end)))))))))
792 fuel)))
793
794def nvidiaPlanHostContains =
795 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
796 (lambda unrestricted host : Nat .
797 (lambda unrestricted extent : Nat .
798 (let unrestricted mappings = (phLayoutMappings layout)
799 in (phCovers mappings (phMappingCount mappings) host extent)))))
800
801-- a GPU-cached buffer is CPU-uncached (MAP_NOT_REQUIRED): no host address
802def phGPUCachedUnmapped =
803 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
804 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat) buffers
805 (branch NvidiaPlanHostBuffersEnd . 1)
806 (branch NvidiaPlanHostBuffersNext head rest induction .
807 (naturalAnd induction (naturalSelect (phBufferIsGPUCached head) (naturalIsZero (phBufferHost head)) 1)))))
808
809-- Admission, 1 when the host will be derived: under direct-RM the USERD
810-- buffer has the target ABI's location (Ampere requires video memory;
811-- the integrated GB10 profile requires system memory). Under
812-- UVM the USERD entry is the alias of the GPFIFO's last page and is not
813-- allocated, so there is nothing to admit. A pairing gates its artifact
814-- on this and the checker decides it.
815def nvidiaPlanHostLayoutAdmitted =
816 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
817 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
818 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
819 (naturalAnd (phGPUCachedUnmapped (phLayoutMappings layout))
820 (naturalSelect (phIsUVM lifecycle) 1
821 (naturalEqual (phBufferIsVideo userd) (phUSERDRequiresVideo abi)))))))
822
823
824-- ---- the layout's placement certificate ----
825-- Every buffer of a layout is a resident of two arenas: the card's virtual
826-- address space (49 bits on Ampere) at its GPU address, and the process's
827-- (47 bits of user space) at its host address when it is mapped there. In
828-- each, Runtime.ArenaCertificate decides every resident page-aligned,
829-- non-empty, inside, and disjoint from every other -- PlanHost's own fixed
830-- mappings (the parameter page, the doorbell) and, under UVM, the channel's
831-- range among them. The one sanctioned alias, the UVM USERD entry (the
832-- GPFIFO buffer's last page, never allocated), is not a resident: it must
833-- lie inside the GPFIFO buffer in both spaces.
834def nvidiaPlanHostPageBytes : Nat = 0x1000
835def phGPUSpaceBytes : Nat = 0x2_0000_0000_0000
836def phHostSpaceBytes : Nat = 0x8000_0000_0000
837
838def phResident =
839 (lambda unrestricted identity : Bytes .
840 (lambda unrestricted offset : Nat .
841 (lambda unrestricted extent : Nat .
842 (lambda unrestricted rest : (family ArenaResidents) .
843 (constructor ArenaResidents ArenaResidentsNext
844 (constructor ArenaResident ArenaResidentValue identity offset extent nvidiaPlanHostPageBytes)
845 rest)))))
846
847-- a buffer at its GPU address
848def phGPUResident =
849 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
850 (lambda unrestricted rest : (family ArenaResidents) .
851 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer
852 (branch NvidiaPlanHostBufferValue identity gpu host extent memory . (phResident identity gpu extent rest)))))
853
854-- a buffer at its host address, when it is mapped (host 0 = not mapped)
855def phHostResident =
856 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
857 (lambda unrestricted rest : (family ArenaResidents) .
858 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents)) buffer
859 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
860 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents))
861 rest
862 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) .
863 (phResident identity host extent rest)))
864 (naturalNonzero host))))))
865
866def phEachResident =
867 (lambda unrestricted place : (pi unrestricted buffer : (family NvidiaPlanHostBuffer) . (pi unrestricted rest : (family ArenaResidents) . (family ArenaResidents))) .
868 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
869 (lambda unrestricted rest : (family ArenaResidents) .
870 (eliminate NvidiaPlanHostBuffers (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (family ArenaResidents)) buffers
871 (branch NvidiaPlanHostBuffersEnd . rest)
872 (branch NvidiaPlanHostBuffersNext head tail induction . (place head induction))))))
873
874-- the layout's buffers, the USERD entry only when it is allocated (direct-RM)
875def phAllocatedBuffers =
876 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
877 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers)) layout
878 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
879 (phMapped gpfifo (phMapped push (phMapped sem (phMapped program (phMapped qmd
880 (nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostBuffers))
881 (phMapped userd data)
882 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family NvidiaPlanHostBuffers) . data))
883 (phIsUVM lifecycle))))))))))
884
885def phGPUResidents =
886 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
887 (phEachResident phGPUResident (phAllocatedBuffers layout)
888 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout
889 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
890 (eliminate NvidiaPlanHostLifecycle (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family ArenaResidents)) lifecycle
891 (branch NvidiaPlanHostDirectRM . (constructor ArenaResidents ArenaResidentsEnd))
892 (branch NvidiaPlanHostUVM base extent .
893 (phResident b"uvm-channel-range" phUVMChannelRangeBase phUVMChannelRangeExtent (constructor ArenaResidents ArenaResidentsEnd))))))))
894
895-- `extras`: the mappings a host adds of its own (the request host's recipe
896-- staging area)
897def phHostResidents =
898 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
899 (lambda unrestricted extras : (family ArenaResidents) .
900 (phEachResident phHostResident (phAllocatedBuffers layout)
901 (phResident b"parameters" phParams 0x10000
902 (phResident b"doorbell" phDoorHost 0x10000
903 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout
904 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
905 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents))
906 extras
907 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family ArenaResidents) .
908 (phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes extras)))
909 (naturalNonzero errorHost)))))))))
910
911-- [inner, inner + innerExtent) inside [outer, outer + outerExtent)
912def phInside =
913 (lambda unrestricted inner : Nat . (lambda unrestricted innerExtent : Nat .
914 (lambda unrestricted outer : Nat . (lambda unrestricted outerExtent : Nat .
915 (naturalAnd (naturalLessOrEqual outer inner)
916 (naturalLessOrEqual (naturalAdd inner innerExtent) (naturalAdd outer outerExtent)))))))
917
918-- under UVM, the USERD entry inside the GPFIFO buffer in both spaces
919def phUSERDAliasInside =
920 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
921 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
922 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
923 (naturalSelect (phIsUVM lifecycle)
924 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) userd
925 (branch NvidiaPlanHostBufferValue aliasIdentity aliasGPU aliasHost aliasExtent aliasMemory .
926 (eliminate NvidiaPlanHostBuffer (lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat) gpfifo
927 (branch NvidiaPlanHostBufferValue identity gpu host extent memory .
928 (naturalAnd (phInside aliasGPU aliasExtent gpu extent) (phInside aliasHost aliasExtent host extent))))))
929 1))))
930
931-- 1 when the layout's placement is certified in both spaces
932def nvidiaPlanHostLayoutCertified =
933 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
934 (lambda unrestricted extras : (family ArenaResidents) .
935 (naturalAnd (arenaCertificate phGPUSpaceBytes (phGPUResidents layout))
936 (naturalAnd (arenaCertificate phHostSpaceBytes (phHostResidents layout extras))
937 (phUSERDAliasInside layout)))))
938
939-- Every upload lands inside a host-mapped buffer of the layout: bytes, or a
940-- file's declared extent. The subagent's RTX 3070 sweep (2026-09-23) found
941-- program tables up to 7936 bytes built into a 4096-byte program buffer and
942-- copied past it at run time -- the kernel never ran; now the build refuses.
943def nvidiaPlanHostFillsAdmitted =
944 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
945 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
946 (eliminate NvidiaPlanHostFills (lambda unrestricted current : (family NvidiaPlanHostFills) . Nat) fills
947 (branch NvidiaPlanHostFillsEnd . 1)
948 (branch NvidiaPlanHostFillBytes host payload rest induction .
949 (naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction))
950 (branch NvidiaPlanHostFillFile host path extent rest induction .
951 (naturalAnd (nvidiaPlanHostContains layout host extent) induction)))))
952
953-- what a plan-derived host needs admitted before it is built
954def nvidiaPlanHostAdmitted =
955 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
956 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
957 (naturalAnd (nvidiaPlanHostLayoutAdmitted layout)
958 (naturalAnd (nvidiaPlanHostLayoutCertified layout (constructor ArenaResidents ArenaResidentsEnd))
959 (nvidiaPlanHostFillsAdmitted layout fills)))))
960
961-- system memory: host-cached, contiguous or noncontiguous as declared. video memory: the local-user
962-- object, write-combined, contiguous, page-aligned.
963-- system memory's attributes: PCI, cached, and contiguous (0x32000000) or,
964-- paged, non-contiguous (0x2A000000)
965def phGPUCachedPageBytes : Nat = 0x10000
966
967-- NV_MEMORY_ALLOCATION_PARAMS for a buffer: owner, flags (8), attr (24),
968-- attr2 (28), format (32), size (64), alignment (72), limit (88)
969def phGPUCachedMemoryParams =
970 (lambda unrestricted extent : Nat .
971 (phSet64 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 128)
972 0 0x636c6161) 8 0x0000C001) 24 0x0B000000) 28 0x00000005) 32 0x00000006)
973 64 extent) 72 phGPUCachedPageBytes) 88 (naturalSaturatingSubtract extent 1)))
974
975
976def phMemoryParams =
977 (lambda unrestricted video : Nat .
978 (lambda unrestricted paged : Nat .
979 (lambda unrestricted cached : Nat .
980 (lambda unrestricted inside : Nat .
981 (lambda unrestricted extent : Nat .
982 (nat-eliminate
983 (lambda unrestricted current : Nat . Bytes)
984 (nat-eliminate
985 (lambda unrestricted current : Nat . Bytes)
986 (phSet64 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 24 (naturalSelect paged 0x2A000000 0x32000000)) 64 extent)
987 (lambda unrestricted predecessor : Nat .
988 (lambda unrestricted ignored : Bytes . (phGPUCachedMemoryParams extent)))
989 cached)
990 (lambda unrestricted predecessor : Nat .
991 (lambda unrestricted ignored : Bytes .
992 (phSet64 (phSet64 (phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x48454C49) 8 0x00008000) 24 (naturalSelect inside 0x58000000 0x50000000)) 64 extent) 72 0x1000)))
993 video))))))
994
995def phMemoryClass =
996 (lambda unrestricted video : Nat . (naturalSelect video 0x40 0x3E))
997
998-- the host mapping of one buffer through a fresh control descriptor, or for
999-- video memory through a fresh card descriptor
1000def phOpenCardsInto =
1001 (lambda unrestricted descriptor : Nat .
1002 (lambda unrestricted path : Bytes .
1003 (lambda unrestricted tail : (family NativePhysicalCommands) .
1004 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotMap)
1005 (phCall phSysIoctl (phArgs3 (phSlot phSlotMap) (phImm phWaitOpen) (phState phWait)) b"" phDiscard
1006 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm descriptor) (phImm 0)) b"" phDiscard tail))))))
1007
1008def phMappingDescriptor =
1009 (lambda unrestricted video : Nat .
1010 (lambda unrestricted tail : (family NativePhysicalCommands) .
1011 (nat-eliminate
1012 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
1013 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotMap)
1014 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdMap) (phImm 0)) b"" phDiscard tail))
1015 (lambda unrestricted predecessor : Nat .
1016 (lambda unrestricted ignored : (family NativePhysicalCommands) .
1017 (phOpenCardsInto phFdMap b"/dev/nvidia0\x00" (phOpenCardsInto phFdMap b"/dev/nvidia1\x00"
1018 (phOpenCardsInto phFdMap b"/dev/nvidia2\x00" (phOpenCardsInto phFdMap b"/dev/nvidia3\x00"
1019 (phOpenCardsInto phFdMap b"/dev/nvidia4\x00" (phOpenCardsInto phFdMap b"/dev/nvidia5\x00"
1020 (phOpenCardsInto phFdMap b"/dev/nvidia6\x00" (phOpenCardsInto phFdMap b"/dev/nvidia7\x00" tail))))))))))
1021 video)))
1022
1023-- the host mapping of one RM memory object: the NVOS33 map through the
1024-- fresh descriptor, its status recorded, then mmap at the host address
1025def phMapMemory =
1026 (lambda unrestricted identity : Bytes .
1027 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1028 (lambda unrestricted block : Nat .
1029 (lambda unrestricted hMemory : Nat .
1030 (lambda unrestricted video : Nat .
1031 (lambda unrestricted extent : Nat .
1032 (lambda unrestricted host : Nat .
1033 (lambda unrestricted statusOffset : Nat .
1034 (lambda unrestricted tail : (family NativePhysicalCommands) .
1035 (let unrestricted flags = (naturalSelect video 0x01010000 0x03008000)
1036 in
1037 (phMappingDescriptor video
1038 (phCall phSysIoctl (phArgs3 (phImm phFdMap) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard
1039 (phCopy block (phSet32 (phSet32 (phSet32 (phSet64 (phSet32 (phSet32 (phZeros 56) 4 phHDevice) 8 hMemory) 24 extent) 40 phStatusSentinel) 44 flags) 48 phFdMap)
1040 (phCopyStateToState block (naturalAdd phRoot 8) 4
1041 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState block)) b"" phDiscard
1042 (phCopyStateToState statusOffset (naturalAdd block 40) 4
1043 (phCheckStateZero32 identity (phTolerate mode) (naturalAdd block 40)
1044 (phCall phSysMmap (phArgs (phImm host) (phImm extent) (phImm 3) (phImm phMapSharedFixed) (phImm phFdMap) (phImm 0)) b"" phDiscard
1045 tail))))))))))))))))))
1046
1047def phHostMap =
1048 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1049 (lambda unrestricted index : Nat .
1050 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1051 (lambda unrestricted tail : (family NativePhysicalCommands) .
1052 (phMapMemory b"host-map" mode (naturalAdd (phBufferState index) 128) (phHMemory index) (phBufferIsVideo buffer)
1053 (phBufferExtent buffer) (phBufferHost buffer) (naturalAdd (phBufferStatus index) 12) tail)))))
1054
1055def phDirectDMAFlags =
1056 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1057 (eliminate NvidiaPlanHostABI (lambda unrestricted current : (family NvidiaPlanHostABI) . Nat) abi
1058 (branch NvidiaPlanHostABIValue mapDMA size dmaOffset status channel compute usermode engine driverBranch scheduleSize userdMemory channelFlags directDMAFlags . directDMAFlags)))
1059
1060-- direct-RM: a fixed virtual reservation and the DMA map to it
1061def phDirectRange =
1062 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1063 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1064 (lambda unrestricted index : Nat .
1065 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1066 (lambda unrestricted tail : (family NativePhysicalCommands) .
1067 (let unrestricted st = (phBufferState index)
1068 in (let unrestricted gpu = (phBufferGPU buffer)
1069 in (let unrestricted extent = (phBufferExtent buffer)
1070 in
1071 (phFill (phVirtP index) (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 (naturalSaturatingSubtract (naturalAdd gpu extent) 1)) 16 phHVASpace)
1072 (phAlloc b"alloc:virtual" (phTolerate mode) (naturalAdd st 32) phHDevice 0x70 (phVirtP index) 24 (phHVirtual index) (naturalAdd (phBufferStatus index) 4)
1073 (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)
1074 (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4
1075 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard
1076 (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4
1077 (phCheckStateZero32 b"dma-map" (phTolerate mode) (naturalAdd st (naturalAdd 64 (phABI abi 3))) tail)))))))))))))))
1078
1079-- NVOS46 flags of the UVM path's DMA map: DMA_OFFSET_FIXED, CACHE_SNOOP,
1080-- and 4 KiB pages; a GPU-cached buffer takes the allocation's own (64 KiB)
1081-- page size instead
1082def phUVMDMAFlags : Nat = 0x8110
1083def phUVMDMAFlagsDefaultPages : Nat = 0x8010
1084
1085-- UVM: an external range at the plan's address, the DMA map through the
1086-- device DMA selector, and the mapping registered with UVM
1087def phUVMRange =
1088 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1089 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1090 (lambda unrestricted inside : Nat .
1091 (lambda unrestricted index : Nat .
1092 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1093 (lambda unrestricted tail : (family NativePhysicalCommands) .
1094 (let unrestricted st = (phBufferState index)
1095 in (let unrestricted gpu = (phBufferGPU buffer)
1096 in (let unrestricted extent = (phBufferExtent buffer)
1097 in (let unrestricted tolerate = (phTolerate mode)
1098 in
1099 (phWhen (naturalIsZero inside)
1100 (lambda unrestricted rest : (family NativePhysicalCommands) .
1101 (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 gpu) 8 extent) 16 phStatusSentinel)
1102 (phUVMCall b"uvm-buffer-range" (naturalAdd 8 (naturalMultiply 2 index)) tolerate phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest)))
1103 (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)
1104 (phCopyStateToState (naturalAdd st 64) (naturalAdd phRoot 8) 4
1105 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm (phABI abi 0)) (phState (naturalAdd st 64))) b"" phDiscard
1106 (phCopyStateToState (naturalAdd (phBufferStatus index) 8) (naturalAdd st (naturalAdd 64 (phABI abi 3))) 4
1107 (phCheckStateZero32 b"dma-map-uvm" tolerate (naturalAdd st (naturalAdd 64 (phABI abi 3)))
1108 (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)
1109 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) (naturalAdd phUVMMapAllocationP 24) 16
1110 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMMapAllocationP 9252) 4
1111 (phUVMCall b"uvm-buffer-map" (naturalAdd 9 (naturalMultiply 2 index)) tolerate phFdUVM phUVMMapExternalAllocation phUVMMapAllocationP 9260 tail))))))))))))))))))))
1112
1113-- One buffer: allocate, place, map.
1114def phBuffer =
1115 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1116 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1117 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1118 (lambda unrestricted index : Nat .
1119 (lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
1120 (lambda unrestricted tail : (family NativePhysicalCommands) .
1121 (let unrestricted video = (phBufferIsVideo buffer)
1122 in (let unrestricted uvm = (phIsUVM lifecycle)
1123 in (let unrestricted inside = (phInsideRange lifecycle (phBufferGPU buffer) (phBufferExtent buffer))
1124 in
1125 (phFill (phMemP index) (phMemoryParams video (phBufferIsPaged buffer) (phBufferIsGPUCached buffer) inside (phBufferExtent buffer))
1126 (phAlloc b"alloc:buffer" (phTolerate mode) (phBufferState index) phHDevice (phMemoryClass video) (phMemP index) 128 (phHMemory index) (phBufferStatus index)
1127 (phWhen (naturalIsZero uvm) (phDirectRange abi mode index buffer)
1128 (phWhen uvm (phUVMRange abi mode inside index buffer)
1129 (phWhen (naturalNonzero (phBufferHost buffer)) (phHostMap mode index buffer)
1130 tail))))))))))))))
1131
1132def phDataBuffers =
1133 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1134 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1135 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1136 (lambda unrestricted first : Nat .
1137 (lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
1138 (lambda unrestricted tail : (family NativePhysicalCommands) .
1139 (app
1140 (eliminate NvidiaPlanHostBuffers
1141 (lambda unrestricted current : (family NvidiaPlanHostBuffers) . (pi unrestricted index : Nat . (family NativePhysicalCommands)))
1142 buffers
1143 (branch NvidiaPlanHostBuffersEnd . (lambda unrestricted index : Nat . tail))
1144 (branch NvidiaPlanHostBuffersNext head rest induction .
1145 (lambda unrestricted index : Nat . (phBuffer abi mode lifecycle index head (induction (succ index))))))
1146 first)))))))
1147
1148-- ---- device discovery ----
1149def phOpenCard =
1150 (lambda unrestricted path : Bytes .
1151 (lambda unrestricted tail : (family NativePhysicalCommands) .
1152 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) path (phStore phSlotGPU)
1153 (phCall phSysIoctl (phArgs3 (phSlot phSlotGPU) (phImm phWaitOpen) (phState phWait)) b"" phDiscard
1154 (phCall phSysDup2 (phArgs3 (phSlot phSlotGPU) (phImm phFdCard) (phImm 0)) b"" phDiscard tail)))))
1155
1156def phDeviceProbe =
1157 (lambda unrestricted index : Nat .
1158 (lambda unrestricted tail : (family NativePhysicalCommands) .
1159 (phFill phDevP (phSet32 (phZeros 56) 0 index)
1160 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phDev)) b"" phDiscard tail))))
1161
1162-- NV2080_CTRL_CMD_GPU_GET_NAME_STRING: the 64 ASCII bytes the card reports
1163-- must equal the name the plan was paired with
1164def phNameWord =
1165 (lambda unrestricted expected : Bytes .
1166 (lambda unrestricted offset : Nat .
1167 (lambda unrestricted tail : (family NativePhysicalCommands) .
1168 (phCopyMappedToState (naturalAdd (naturalAdd phNameP 4) offset) phScratch 8
1169 (phCopy (naturalAdd phScratch 8) (phTake 8 (phDrop offset expected))
1170 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phLoad (naturalAdd phScratch 8)) phIdentity tail))))))
1171
1172def phExpectName =
1173 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1174 (lambda unrestricted expected : Bytes .
1175 (lambda unrestricted tail : (family NativePhysicalCommands) .
1176 (phFill phNameP (phZeros 132)
1177 (phControl b"control:phName" (phTolerate mode) (phRMStatusSlot 11) phName phHSubdevice 0x20800110 phNameP 132
1178 (phNameWord expected 0 (phNameWord expected 8 (phNameWord expected 16 (phNameWord expected 24
1179 (phNameWord expected 32 (phNameWord expected 40 (phNameWord expected 48 (phNameWord expected 56 tail)))))))))))))
1180
1181-- ---- the UVM driver ----
1182def phUVMPrepare =
1183 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1184 (lambda unrestricted base : Nat .
1185 (lambda unrestricted extent : Nat .
1186 (lambda unrestricted tail : (family NativePhysicalCommands) .
1187 (phFill phUVMGidP (phSet32 (phSet32 (phZeros 268) 4 2) 8 16)
1188 (phControl b"control:phUVMControl" (phTolerate mode) (phRMStatusSlot 12) phUVMControl phHSubdevice 0x2080014A phUVMGidP 268
1189 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap)
1190 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVM) (phImm 0)) b"" (phStore phSlotMap)
1191 (phFill phUVMInitP (phSet32 (phZeros 16) 8 phStatusSentinel)
1192 (phUVMCallAfterOpen (phTolerate mode) b"uvm-initialize" 1 (phTolerate mode) phFdUVM phUVMInitialize phUVMInitP 8
1193 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidia-uvm\x00" (phStore phSlotMap)
1194 (phCall phSysDup2 (phArgs3 (phSlot phSlotMap) (phImm phFdUVMMemoryMap) (phImm 0)) b"" (phStore phSlotMap)
1195 (phFill phUVMMMP (phSet32 (phSet32 (phZeros 8) 0 phFdUVM) 4 phStatusSentinel)
1196 (phUVMCallAfterOpen (phTolerate mode) b"uvm-mm-initialize" 2 1 phFdUVMMemoryMap phUVMMMInitialize phUVMMMP 4
1197 (phFill phUVMRegisterGPUP (phSet32 (phSet32 (phZeros 40) 24 phStatusSentinel) 36 phStatusSentinel)
1198 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterGPUP 16
1199 (phUVMCall b"uvm-register-gpu" 3 (phTolerate mode) phFdUVM phUVMRegisterGPU phUVMRegisterGPUP 36
1200 (phFill phUVMRegisterVASpaceP (phSet32 (phSet32 (phSet32 (phZeros 32) 16 phFdControl) 24 phHVASpace) 28 phStatusSentinel)
1201 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterVASpaceP 16
1202 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterVASpaceP 20) 4
1203 (phUVMCall b"uvm-register-vaspace" 4 (phTolerate mode) phFdUVM phUVMRegisterGPUVASpace phUVMRegisterVASpaceP 28
1204 (phWhen (naturalNonzero extent)
1205 (lambda unrestricted rest : (family NativePhysicalCommands) .
1206 (phFill phUVMCreateRangeP (phSet32 (phSet64 (phSet64 (phZeros 24) 0 base) 8 extent) 16 phStatusSentinel)
1207 (phUVMCall b"uvm-external-range" 6 (phTolerate mode) phFdUVM phUVMCreateExternalRange phUVMCreateRangeP 16 rest)))
1208 tail))))))))))))))))))))))
1209
1210def phUVMRegisterChannelCommands =
1211 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1212 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1213 (lambda unrestricted tail : (family NativePhysicalCommands) .
1214 (phFill phUVMRegisterChannelP (phSet32 (phSet64 (phSet64 (phSet32 (phSet32 (phZeros 56) 16 phFdControl) 24 (phHClass (phABI abi 4))) 32 phUVMChannelRangeBase) 40 phUVMChannelRangeExtent) 48 phStatusSentinel)
1215 (phCopyMappedToMapped (naturalAdd phUVMGidP 12) phUVMRegisterChannelP 16
1216 (phCopyStateToMapped (naturalAdd phRoot 8) (naturalAdd phUVMRegisterChannelP 20) 4
1217 (phUVMCall b"uvm-register-channel" 5 (phTolerate mode) phFdUVM phUVMRegisterChannel phUVMRegisterChannelP 48 tail)))))))
1218
1219-- ---- publishing a submission ----
1220-- gpPut into USERD, SFENCE, the work-submit token into the doorbell: the
1221-- training runtime's publication routine (x86: mov [rdi], esi; sfence;
1222-- mov [rdx], ecx), run on this thread, so the doorbell cannot reach the card
1223-- ahead of gpPut through a write-combining buffer. The token is loaded
1224-- from the parameter page into the scratch word first.
1225--
1226-- Measured on an RTX 3090, driver 580.178.04, 2026-09-24. Before, gpPut
1227-- went through the pipe copy and the doorbell after it, unordered: 7 hangs
1228-- in 250 warp-sum runs, and in every one the semaphores were untouched (the
1229-- device never began the pushbuffer), USERD's GP_PUT 1 and GP_GET 0 (the
1230-- channel never fetched the entry) -- the doorbell had arrived before
1231-- gpPut. A membarrier between the two (a locked-instruction barrier, which
1232-- need not drain write-combining buffers) did not help: 11 hangs in 300
1233-- against 6 unfenced. This routine: 0 hangs in 300 against 13 unfenced,
1234-- interleaved on the same card.
1235def phPublishCode : Bytes =
1236 (eliminate X86NativeAssemblyResult (lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
1237 nativePhysicalTrainingGeneratePublish32Routine
1238 (branch X86NativeAssemblyEncoded code . code)
1239 (branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
1240 (branch X86NativeAssemblyEncodeOffsetOverflow . b"")
1241 (branch X86NativeAssemblyMissingLabel name . b"")
1242 (branch X86NativeAssemblyDisplacementOutOfRange name . b""))
1243
1244def phLoadToken =
1245 (lambda unrestricted tail : (family NativePhysicalCommands) .
1246 (phCopy phScratch (phZeros 8)
1247 (phCopyMappedToState phTokP phScratch 4 tail)))
1248
1249def phPublishOperand =
1250 (lambda unrestricted userdGPPut : Nat .
1251 (lambda unrestricted gpPut : (family NativePhysicalOperand) .
1252 (lambda unrestricted tail : (family NativePhysicalCommands) .
1253 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine phPublishCode
1254 (phArgs (phImm userdGPPut) gpPut (phImm (naturalAdd phDoorHost 0x90)) (phLoad phScratch) (phImm 0) (phImm 0))
1255 phDiscard)
1256 tail))))
1257
1258def phPublish =
1259 (lambda unrestricted userdGPPut : Nat . (lambda unrestricted gpPut : Nat . (phPublishOperand userdGPPut (phImm gpPut))))
1260
1261-- ---- the doorbell ----
1262def phDoorbell =
1263 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1264 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1265 (lambda unrestricted tail : (family NativePhysicalCommands) .
1266 (phCall phSysIoctl (phArgs3 (phImm phFdCard) (phImm phRegisterFD) (phImm phRegFdP)) b"" phDiscard
1267 (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)
1268 (phCopyStateToState phDoorMap (naturalAdd phRoot 8) 4
1269 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState phDoorMap)) b"" phDiscard
1270 (phCopyStateToState (phRMStatusSlot 18) (naturalAdd phDoorMap 40) 4
1271 (phCheckStateZero32 b"doorbell-map" (phTolerate mode) (naturalAdd phDoorMap 40)
1272 (phCall phSysMmap (phArgs (phImm phDoorHost) (phImm 0x10000) (phImm 3) (phImm phMapSharedFixed) (phImm phFdCard) (phImm 0)) b"" phDiscard tail))))))))))
1273
1274def phToken =
1275 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1276 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1277 (lambda unrestricted tail : (family NativePhysicalCommands) .
1278 (phFill phTokP (phZeros 4)
1279 (phControl b"control:phTok" (phTolerate mode) (phRMStatusSlot 15) phTok (phHClass (phABI abi 4)) 0xc36f0108 phTokP 4 tail)))))
1280
1281def phSchedule =
1282 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1283 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1284 (lambda unrestricted tail : (family NativePhysicalCommands) .
1285 (phFill phSchedP (phTake (phABI abi 9) (bytes 1 0 0))
1286 (phControl b"control:phSched" (phTolerate mode) (phRMStatusSlot 14) phSched phHGroup 0xa06c0101 phSchedP (phABI abi 9) tail)))))
1287
1288def phVASpaceParams =
1289 (lambda unrestricted uvm : Nat .
1290 (nat-eliminate
1291 (lambda unrestricted current : Nat . Bytes)
1292 (phZeros 48)
1293 (lambda unrestricted predecessor : Nat .
1294 (lambda unrestricted ignored : Bytes . (phSet64 (phSet64 (phSet32 (phZeros 48) 4 0x48) 8 0x1FFFFFB000000) 40 0x1000)))
1295 uvm))
1296
1297def phUVMLifecycle =
1298 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1299 (lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
1300 (lambda unrestricted tail : (family NativePhysicalCommands) .
1301 (eliminate NvidiaPlanHostLifecycle
1302 (lambda unrestricted current : (family NvidiaPlanHostLifecycle) . (family NativePhysicalCommands))
1303 lifecycle
1304 (branch NvidiaPlanHostDirectRM . tail)
1305 (branch NvidiaPlanHostUVM base extent . (phUVMPrepare mode base extent tail))))))
1306
1307def phDMASelector =
1308 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1309 (lambda unrestricted tail : (family NativePhysicalCommands) .
1310 (phFill phDMAObjectP (phSet64 (phZeros 24) 8 0x1FFFFFFFFFFFF)
1311 (phAlloc b"alloc:phDMAObject" (phTolerate mode) phDMAObject phHDevice 0x70 phDMAObjectP 24 phHDMA (phRMStatusSlot 2) tail))))
1312
1313def phDirectActivate =
1314 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1315 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1316 (lambda unrestricted tail : (family NativePhysicalCommands) .
1317 (phFill phBindP (phW32 1)
1318 (phControl b"control:phBind" (phTolerate mode) (phRMStatusSlot 13) phBind (phHClass (phABI abi 4)) 0xa06f0104 phBindP 4
1319 (phSchedule abi mode (phToken abi mode (phDoorbell abi mode tail))))))))
1320
1321def phUVMActivate =
1322 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1323 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1324 (lambda unrestricted tail : (family NativePhysicalCommands) .
1325 (phDoorbell abi mode
1326 (phFill phPreemptP (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 0 1) 4 phHGroup) 8 0) 12 2)
1327 (phControl b"control:phPreempt" (phTolerate mode) (phRMStatusSlot 16) phPreempt phHSubdevice 0x20801210 phPreemptP 32
1328 (phToken abi mode (phUVMRegisterChannelCommands abi mode (phSchedule abi mode tail)))))))))
1329
1330-- the UVM lifecycle's GPFIFO: 0x8000 entries of 8 bytes in the video GPFIFO
1331-- buffer, USERD the page after them
1332def nvidiaPlanHostUVMGPFIFOEntries : Nat = 0x8000
1333def nvidiaPlanHostUVMGPFIFOBytes : Nat = (naturalMultiply nvidiaPlanHostUVMGPFIFOEntries 8)
1334
1335-- Where a plan maps its buffers in the process: from the origin, each
1336-- after the previous at the alignment, in extents of the mapping unit.
1337-- The host side of the arena certificate decides that they are disjoint
1338-- and clear of the host's own mappings.
1339def nvidiaPlanHostMappingOrigin : Nat = 0x6000_0000
1340def nvidiaPlanHostMappingAlignment : Nat = 0x0200_0000
1341def nvidiaPlanHostMappingUnit : Nat = 0x10000
1342
1343-- the USERD page mapped after the GPFIFO entries, and the words of it the
1344-- host reads: GP_GET and GP_PUT (Accelerator.SM86.USERD's layout, slot 0)
1345def nvidiaPlanHostUSERDBytes : Nat = nvidiaPlanHostPageBytes
1346def nvidiaPlanHostUSERDGPGetOffset : Nat = 0x88
1347def nvidiaPlanHostUSERDGPPutOffset : Nat = 0x8c
1348def nvidiaPlanHostDirectGPFIFOEntries : Nat = 0x400
1349
1350def phChannelParams =
1351 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1352 (lambda unrestricted direct : Nat .
1353 (lambda unrestricted gpfifoGPU : Nat .
1354 (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)))))
1355
1356-- ---- the driver's branch ----
1357-- NV_ESC_CHECK_VERSION_STR (0xD2, 72 bytes: cmd, reply, 64 version bytes)
1358-- with cmd '2', query: the driver writes its own version string. Its first
1359-- four bytes must be the branch the host's ABI was built for, or the host
1360-- stops, naming `driver-branch`, before any card call -- a 580-ABI host on a
1361-- 575 driver used to run until its DMA map failed (exit 120 at `dma-map`),
1362-- and on a 570 driver it faulted. Measured on the RTX 3090, 2026-09-24:
1363-- driver 580.178.04 answers `580.178.04`, reply 1. A driver that does not
1364-- answer leaves the bytes zero and is refused the same way.
1365def phCheckVersionIoctl : Nat = 0xC04846D2
1366def phVersion : Nat = 1024
1367
1368def phRootAndDriverBranch =
1369 (lambda unrestricted abi : (family NvidiaPlanHostABI) .
1370 (lambda unrestricted offset : Nat .
1371 (lambda unrestricted tail : (family NativePhysicalCommands) .
1372 (phAssertStateZero32 b"root" offset
1373 (phCopy phVersion (phSet32 (phZeros 72) 0 0x32)
1374 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phCheckVersionIoctl) (phState phVersion)) b"" phDiscard
1375 (phCopy phScratch (phZeros 8)
1376 (phCopyStateToState phScratch (naturalAdd phVersion 8) 4
1377 (nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm (phABI abi 8)) b"driver-branch" tail)))))))))
1378
1379-- ---- the prelude: a working compute channel ----
1380def phPrelude =
1381 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1382 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1383 (lambda unrestricted tail : (family NativePhysicalCommands) .
1384 (eliminate NvidiaPlanHostLayout
1385 (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NativePhysicalCommands))
1386 layout
1387 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
1388 (let unrestricted uvm = (phIsUVM lifecycle)
1389 in (let unrestricted direct = (naturalIsZero uvm)
1390 in (let unrestricted channelClass = (phHClass (phABI abi 4))
1391 in (let unrestricted tolerate = (phTolerate mode)
1392 in
1393 (phOpenCard b"/dev/nvidia0\x00" (phOpenCard b"/dev/nvidia1\x00" (phOpenCard b"/dev/nvidia2\x00" (phOpenCard b"/dev/nvidia3\x00"
1394 (phOpenCard b"/dev/nvidia4\x00" (phOpenCard b"/dev/nvidia5\x00" (phOpenCard b"/dev/nvidia6\x00" (phOpenCard b"/dev/nvidia7\x00"
1395 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags)) b"/dev/nvidiactl\x00" (phStore phSlotControl)
1396 (phCall phSysDup2 (phArgs3 (phSlot phSlotControl) (phImm phFdControl) (phImm 0)) b"" phDiscard
1397 (phCopy phRoot (phSet32 (phZeros 32) 28 phStatusSentinel)
1398 (phCall phSysIoctl (phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phRoot)) b"" phDiscard
1399 (phCopyStateToState (phRMStatusSlot 0) (naturalAdd phRoot 28) 4
1400 (phRootAndDriverBranch abi (naturalAdd phRoot 28)
1401 (phCall phSysMmap (phArgs (phImm phParams) (phImm 0x10000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard
1402 (phFill phRegFdP (phW32 phFdControl)
1403 (phCopy phDev (phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 8 phHDevice) 12 0x80) 16 phDevP) 24 56)
1404 (phCopyStateToState phDev (naturalAdd phRoot 8) 4
1405 (phCopyStateToState (naturalAdd phDev 4) (naturalAdd phRoot 8) 4
1406 (phDeviceProbe 0 (phDeviceProbe 1 (phDeviceProbe 2 (phDeviceProbe 3
1407 (phDeviceProbe 4 (phDeviceProbe 5 (phDeviceProbe 6 (phDeviceProbe 7
1408 (phFill phSubP (phZeros 4)
1409 (phAlloc b"alloc:phSub" tolerate phSub phHDevice 0x2080 phSubP 4 phHSubdevice (phRMStatusSlot 1)
1410 (phWhen (naturalNonzero (bytes-length expectedName)) (phExpectName mode expectedName)
1411 (phWhen uvm (phDMASelector mode)
1412 (phFill phVASP (phVASpaceParams uvm)
1413 (phAlloc b"alloc:phVAS" tolerate phVAS phHDevice 0x90f1 phVASP 48 phHVASpace (phRMStatusSlot 3)
1414 (phUVMLifecycle mode lifecycle
1415 (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
1416 (phWhen direct (phBuffer abi mode lifecycle 5 userd)
1417 (phDataBuffers abi mode lifecycle 6 data
1418 (phFill phErrP (phMemoryParams 0 0 0 0 0x1000)
1419 (phAlloc b"alloc:phErr" tolerate phErr phHDevice 0x3E phErrP 128 phHError (phRMStatusSlot 4)
1420 (phWhen (naturalNonzero errorHost) (phMapMemory b"error-map" mode phErrMap phHError 0 0x1000 errorHost (phRMStatusSlot 7))
1421 (phFill phGroupP (phSet32 (phSet32 (phZeros 20) 8 (naturalSelect direct phHVASpace 0)) 12 1)
1422 (phAlloc b"alloc:phGroup" tolerate phGroup phHDevice 0xa06c phGroupP 20 phHGroup (phRMStatusSlot 5)
1423 (phFill phCtxP (phSet32 (phSet32 (phZeros 12) 0 phHVASpace) 4 uvm)
1424 (phAlloc b"alloc:phCtx" tolerate phCtx phHGroup 0x9067 phCtxP 12 phHContext (phRMStatusSlot 6)
1425 (phFill phChanP (phChannelParams abi direct (phBufferGPU gpfifo))
1426 (phAlloc b"alloc:phChan" tolerate phChan phHGroup (phABI abi 4) phChanP 368 channelClass (phRMStatusSlot 8)
1427 (phAlloc b"alloc:phComp" tolerate phComp channelClass (phABI abi 5) 0 0 (phHClass (phABI abi 5)) (phRMStatusSlot 9)
1428 (phAlloc b"alloc:phUser" tolerate phUser phHSubdevice (phABI abi 6) 0 0 (phHClass (phABI abi 6)) (phRMStatusSlot 10)
1429 (phWhen direct (phDirectActivate abi mode)
1430 (phWhen uvm (phUVMActivate abi mode)
1431 tail)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1432
1433-- ---- uploads, submission, completion, readback ----
1434def phFills =
1435 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
1436 (lambda unrestricted tail : (family NativePhysicalCommands) .
1437 (eliminate NvidiaPlanHostFills
1438 (lambda unrestricted current : (family NvidiaPlanHostFills) . (family NativePhysicalCommands))
1439 fills
1440 (branch NvidiaPlanHostFillsEnd . tail)
1441 (branch NvidiaPlanHostFillBytes host payload rest induction . (phFill host payload induction))
1442 (branch NvidiaPlanHostFillFile host path extent rest induction . (phReadFile path host extent induction)))))
1443
1444def phReads =
1445 (lambda unrestricted reads : (family NvidiaPlanHostReads) .
1446 (lambda unrestricted tail : (family NativePhysicalCommands) .
1447 (eliminate NvidiaPlanHostReads
1448 (lambda unrestricted current : (family NvidiaPlanHostReads) . (family NativePhysicalCommands))
1449 reads
1450 (branch NvidiaPlanHostReadsEnd . tail)
1451 (branch NvidiaPlanHostReadsNext host extent rest induction .
1452 (phCall phSysWrite (phArgs3 (phImm 1) (phImm host) (phImm extent)) b"" phDiscard induction)))))
1453
1454def nvidiaPlanHostFenceValue : Nat = 65261
1455def nvidiaPlanHostFenceInterval : Nat = 1000000
1456def nvidiaPlanHostFenceMaximumPolls : Nat = 600000
1457
1458def phUSERDHost =
1459 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1460 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
1461 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
1462 (phBufferHost userd))))
1463
1464-- Release everything before exit: freeing the root client tears the whole
1465-- object hierarchy down synchronously. Left to the driver's asynchronous
1466-- reclaim at process exit, back-to-back hosts on the RTX 3090 hit
1467-- NV_ERR_INSUFFICIENT_RESOURCES on the channel allocation about a third of
1468-- the time, in streaks; v3 of this host, which did not free, did too.
1469def phRelease =
1470 (lambda unrestricted tail : (family NativePhysicalCommands) .
1471 (phCopy phFree (phSet32 (phZeros 16) 12 phStatusSentinel)
1472 (phCopyStateToState phFree (naturalAdd phRoot 8) 4
1473 (phCopyStateToState (naturalAdd phFree 4) (naturalAdd phRoot 8) 4
1474 (phCopyStateToState (naturalAdd phFree 8) (naturalAdd phRoot 8) 4
1475 (phCall phSysIoctl (phArgs3 (phImm phFdControl) (phImm phRMFree) (phState phFree)) b"" phDiscard
1476 (phCopyStateToState (phRMStatusSlot 17) (naturalAdd phFree 12) 4
1477 (phAssertStateZero32 b"rm-free-root" (naturalAdd phFree 12) tail))))))))
1478
1479-- The whole host, Strict: `submissions` is gpPut, the number of GPFIFO
1480-- entries the plan's tables carry; `fenceHost` the host address of the
1481-- semaphore slot the last submission releases; `statusHost`, when not 0, a
1482-- mapped address the UVM status record is copied to before the readbacks.
1483-- ---- native telemetry (docs/observability PRD item 9) ----
1484-- At each phase boundary the host appends an ALPHATEL record to
1485-- `alpha-host.alphatel` in its working directory: the body is
1486-- Runtime.NativeTelemetry's own encoding, made at build time (domain 1,
1487-- event 1 "reached", the boundary's ordinal as phase and sequence, status
1488-- 0, its name as payload), with the monotonic nanoseconds left zero; at
1489-- run time the host reads CLOCK_MONOTONIC and Runtime.NativeTelemetrySeal
1490-- writes the reading into the body, digests it and writes the record. A
1491-- record exists only if the host got there, so the last one names how far
1492-- a failed run came. The write is asserted whole (`telemetry-write`): a
1493-- host that cannot record says so and stops, rather than running unobserved.
1494-- Its pages: a fixed anonymous mapping of its own, taken before any device
1495-- call, so a host with no card still records its beginning.
1496def phTelemetryPage : Nat = 0x5E000000
1497def phTelemetryPadded : Nat = 0x5E000000
1498def phTelemetryRecord : Nat = 0x5E000400
1499def phTelemetryClock : Nat = 0x5E000800
1500def phTelemetryWork : Nat = 0x5E000C00
1501def phSlotTelemetry : Nat = 14
1502def phSlotTelemetryWritten : Nat = 15
1503def phTelemetryPath : Bytes = b"alpha-host.alphatel\x00"
1504def phSysClockGettime : Nat = 228
1505def phClockMonotonic : Nat = 1
1506-- O_WRONLY | O_CREAT | O_APPEND, mode 0600
1507def phTelemetryOpenFlags : Nat = 1089
1508def phTelemetryMode : Nat = 384
1509
1510def phTelemetryIdentity : Bytes = (bytes-append phIdentity (phZeros (naturalSaturatingSubtract nativeTelemetryDigestBytes (bytes-length phIdentity))))
1511def phTelemetryZero : (family ModelWord64) = (phWord 0)
1512
1513-- the body Runtime.NativeTelemetry encodes for boundary `ordinal`, its
1514-- clock reading zero: no error code, the name as payload
1515def phTelemetryBody =
1516 (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes .
1517 (nativeTelemetryRecordBody (phWord ordinal) phTelemetryZero (byte 1) (byte 1) (nat-to-byte ordinal) (byte 0)
1518 (constructor NativeTelemetryCounters NativeTelemetryCountersValue
1519 phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero phTelemetryZero)
1520 phTelemetryIdentity b"" name phTelemetryZero (phWord (bytes-length name)))))
1521
1522-- the body with SHA-256's padding: 0x80, zeros to 56 mod 64, the bit length
1523-- (big-endian; a body is far below 8 KiB)
1524def phTelemetryPadding =
1525 (lambda unrestricted length : Nat .
1526 (bytes-cons (byte 128)
1527 (bytes-append (phZeros (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd 55 512) length) 64))
1528 (bytes-append (phZeros 6)
1529 (bytes-cons (nat-to-byte (naturalDivideUnchecked (naturalMultiply 8 length) 256))
1530 (bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalMultiply 8 length) 256)) b""))))))
1531
1532-- map the telemetry page and put the magic in the record buffer
1533def phTelemetryOpen =
1534 (lambda unrestricted tail : (family NativePhysicalCommands) .
1535 (phCall phSysMmap (phArgs (phImm phTelemetryPage) (phImm 0x1000) (phImm 3) (phImm phMapAnonymousFixed) (phImm phNoDescriptor) (phImm 0)) b"" phDiscard
1536 (phFill phTelemetryRecord b"ALPHATEL" tail)))
1537
1538-- boundary `ordinal`, named: seal and append its record
1539def phTelemetry =
1540 (lambda unrestricted ordinal : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) .
1541 (let unrestricted body = (phTelemetryBody ordinal name)
1542 in (let unrestricted length = (bytes-length body)
1543 in (let unrestricted padded = (bytes-append body (phTelemetryPadding length))
1544 in (phFill phTelemetryPadded padded
1545 (phCall phSysClockGettime (phArgs3 (phImm phClockMonotonic) (phImm phTelemetryClock) (phImm 0)) b"" phDiscard
1546 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetrySealRoutine
1547 (phArgs (phImm phTelemetryPadded) (phImm (naturalDivideUnchecked (bytes-length padded) 64)) (phImm phTelemetryRecord)
1548 (phImm length) (phImm phTelemetryClock) (phImm phTelemetryWork))
1549 phDiscard)
1550 (phCall phSysOpenat (phArgs (phImm phAtFdCwd) phPayload (phImm phTelemetryOpenFlags) (phImm phTelemetryMode) (phImm 0) (phImm 0)) phTelemetryPath (phStore phSlotTelemetry)
1551 (phCall phSysWrite (phArgs3 (phSlot phSlotTelemetry) (phImm phTelemetryRecord) (phImm (naturalAdd 72 length))) b"" (phStore phSlotTelemetryWritten)
1552 (nativeLaunchRecipeAssertEqual (phSlot phSlotTelemetryWritten) (phImm (naturalAdd 72 length)) b"telemetry-write"
1553 (phCall phSysClose (phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0)) b"" phDiscard tail)))))))))))))
1554
1555-- Preparation has two ordered phases: envelope validation before any card
1556-- call, and expansion after the buffers exist. Keeping these continuations
1557-- here gives recipe-backed probes the same telemetry and submit/wait path
1558-- as the ordinary host, without copying its RM command stream.
1559def nvidiaPlanHostPreparedCommands =
1560 (lambda unrestricted before : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1561 (lambda unrestricted mapped : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1562 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1563 (lambda unrestricted fills : (family NvidiaPlanHostFills) .
1564 (lambda unrestricted submissions : Nat .
1565 (lambda unrestricted fenceHost : Nat .
1566 (lambda unrestricted statusHost : Nat .
1567 (lambda unrestricted reads : (family NvidiaPlanHostReads) .
1568 (phPipeCreate
1569 (phTelemetryOpen (phTelemetry 0 b"plan-host:begin"
1570 (before (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout
1571 (phTelemetry 1 b"plan-host:channel-ready"
1572 (mapped (phFills fills
1573 (phTelemetry 2 b"plan-host:uploaded"
1574 (phLoadToken
1575 (phPublish (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) submissions
1576 (phTelemetry 3 b"plan-host:submitted"
1577 (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait (phImm fenceHost) (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval))
1578 (phTelemetry 4 b"plan-host:completed"
1579 (phWhen (naturalNonzero statusHost) (phCopyStateToMapped phUVMStatusRecord statusHost phUVMStatusRecordExtent)
1580 (phReads reads
1581 (phTelemetry 5 b"plan-host:read-back"
1582 (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
1583 (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
1584 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))))))))))))))))))))))))
1585
1586def phNoPreparation =
1587 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)
1588
1589def nvidiaPlanHostCommands =
1590 (nvidiaPlanHostPreparedCommands phNoPreparation phNoPreparation)
1591
1592-- The channel probe, Probe mode: the prelude alone, every status after the
1593-- root client's recorded and none asserted, then to stdout the status area
1594-- -- the 16-byte record per buffer, the UVM slots, the RM slots -- from the
1595-- state and the channel allocation's parameter block as the driver left it
1596-- (its `cid` word at 132 is the hardware channel identifier), then the root
1597-- freed. With a card it prints both and exits 0 whether or not the channel
1598-- came up; which call refused is read off the area.
1599def phProbeRecord : Nat = (phBufferStatus 0)
1600def phProbeRecordExtent : Nat = (naturalSaturatingSubtract (phBufferState 0) (phBufferStatus 0))
1601def phChannelParamsExtent : Nat = 368
1602
1603def nvidiaPlanHostProbeCommands =
1604 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1605 (phPipeCreate
1606 (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostProbe) layout
1607 (phCall phSysWrite (phArgs3 (phImm 1) (phState phProbeRecord) (phImm phProbeRecordExtent)) b"" phDiscard
1608 (phCall phSysWrite (phArgs3 (phImm 1) (phImm phChanP) (phImm phChannelParamsExtent)) b"" phDiscard
1609 (phRelease
1610 (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
1611 (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
1612 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))
1613
1614def phCommandCount =
1615 (lambda unrestricted commands : (family NativePhysicalCommands) .
1616 (eliminate NativePhysicalCommands
1617 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
1618 commands
1619 (branch NativePhysicalCommandsEnd . zero)
1620 (branch NativePhysicalCommandsNext head tail induction . (succ induction))))
1621
1622-- The number of assertions a command list carries: what a mode decides.
1623def phOperationIsAssert =
1624 (lambda unrestricted operation : (family NativePhysicalOperation) .
1625 (eliminate NativePhysicalOperation
1626 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1627 operation
1628 (branch NativePhysicalSystemCall number argv payload result . 0)
1629 (branch NativePhysicalCopyPayloadToState destination extent payload . 0)
1630 (branch NativePhysicalMachineRoutine code argv result . 0)
1631 (branch NativePhysicalFencePoll address expected polls . 0)
1632 (branch NativePhysicalTelemetryAppend path record . 0)
1633 (branch NativePhysicalAssertEqual left right error . 1)
1634 (branch NativePhysicalAssertOneOf observed first second error . 1)
1635 (branch NativePhysicalHaltSuccess . 0)
1636 (branch NativePhysicalRepeatBegin count . 0)
1637 (branch NativePhysicalRepeatEnd . 0)
1638 (branch NativePhysicalStoreWord64 destination value . 0)
1639 (branch NativePhysicalFenceWait address expected polls interval . 0)
1640 (branch NativePhysicalRepeatBeginCounted count . 0)
1641 (branch NativePhysicalAddWord64 destination left right . 0)
1642 (branch NativePhysicalFloat64 operation destination left right . 0)))
1643
1644def phCommandIsAssert =
1645 (lambda unrestricted command : (family NativePhysicalCommand) .
1646 (eliminate NativePhysicalCommand
1647 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
1648 command
1649 (branch NativePhysicalCommandValue operation identity . (phOperationIsAssert operation))))
1650
1651def nvidiaPlanHostAssertionCount =
1652 (lambda unrestricted commands : (family NativePhysicalCommands) .
1653 (eliminate NativePhysicalCommands
1654 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
1655 commands
1656 (branch NativePhysicalCommandsEnd . zero)
1657 (branch NativePhysicalCommandsNext head tail induction . (naturalAdd (phCommandIsAssert head) induction))))
1658
1659-- the prelude alone under a mode, for the assertion contracts
1660def nvidiaPlanHostPreludeCommands =
1661 (lambda unrestricted mode : (family NvidiaPlanHostMode) .
1662 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1663 (phPrelude mode layout (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
1664
1665def nvidiaPlanHostProgram =
1666 (lambda unrestricted identity : Bytes .
1667 (lambda unrestricted commands : (family NativePhysicalCommands) .
1668 (constructor NativePhysicalProgram NativePhysicalProgramValue (phWord phStateExtent) (phWord phSlots) commands (phCommandCount commands) identity zero)))
1669
1670def nvidiaPlanHostELF =
1671 (lambda unrestricted identity : Bytes .
1672 (lambda unrestricted commands : (family NativePhysicalCommands) .
1673 (nativePhysicalGenerateNativeELFBytesDirect (nvidiaPlanHostProgram identity commands))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.