Large source region · 4,856 lines
module Platform.Linux.Nvidia.PlanHost
import Data.Bytes
import Platform.Linux.Nvidia.DeviceBinding
import Runtime.NativeBranch
import Runtime.NativeDescriptor
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.ArenaCertificate
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativeTelemetry
import Runtime.NativeTelemetrySeal
import Runtime.NativePhysicalProgram
import Runtime.NativePhysicalNativeELF
import Runtime.NativePhysicalTrainingRoutine
import Std.Natural
-- The host the compiler derives from a whole-program plan: the compute-channel
-- protocol the SM86 launch ladder proved on the RTX 3070 and the RTX 3090
-- (rungs D..Q, Coppelius S5, the checked linear step), as typed command
-- builders parameterised by the plan's placement. Every address, extent and
-- handle is a parameter or derived from one; the protocol is stated once,
-- here, for every plan.
--
-- Two lifecycles, selected by the layout:
-- direct-RM every buffer is system memory; its GPU range is a fixed RM
-- virtual reservation and a DMA map; the channel has 0x400
-- entries and its own USERD buffer.
-- UVM RM's VA space is duplicated into the UVM driver; buffers are
-- external ranges mapped through it; video-memory buffers are
-- allowed and are not host-mapped; the GPFIFO is one contiguous
-- video allocation whose last page is USERD; the channel is
-- registered with UVM and scheduled last. This is the
-- lifecycle the Coppelius training executables run.
--
-- In order: open the card and the control node; root, device, subdevice,
-- UVM: the DMA selector, the VA space, UVM: initialise the driver, register
-- the GPU and the VA space, reserve the external range; the fixed buffers
-- GPFIFO, pushbuffer, semaphores, program, QMD, direct-RM: USERD, and every
-- data buffer; the error notifier; channel group, context share, channel,
-- compute and usermode objects; direct-RM: bind, schedule, token, doorbell;
-- UVM: doorbell, preemption, token, register the channel, schedule. Then
-- the uploads, gpPut, the doorbell, a FenceWait on the plan's semaphore, the
-- readbacks to stdout, exit 0. Every driver status is pre-set to a sentinel
-- and recorded after the call; under NvidiaPlanHostStrict (the executables)
-- each is asserted zero too, so a host without a card stops at its first
-- device call with a command failure; under NvidiaPlanHostProbe (the
-- channel probe) none after the root's is, and the host prints the status
-- area. The root client is freed before exit.
--
-- Measured on the RTX 3090, driver 580.126.09, 2026-09-22, the checked
-- linear step: UVM lifecycle 11/11 runs; two submissions per host, one
-- semaphore slot each: 6/6, both slots released with timestamps. The
-- direct-RM channel allocation used to fail NV_ERR_INSUFFICIENT_RESOURCES
-- 0x1e intermittently, in streaks, at a rate that drifted with the host
-- machine's other tenants (3/10 .. 17/60). Root-caused 2026-09-23 with the
-- channel probe, one placement at a time interleaved with the baseline:
-- the cause is USERD as a separate SYSTEM-memory allocation. Not the
-- channel flags, the bind, the schedule, the root free, the work, the
-- GPFIFO's memory or the error notifier's (each within noise of the
-- baseline); USERD in video memory 0/60 against 17/60, and the step with
-- USERD in video memory 60/60 records bit-identical against 6/60 failures
-- of the old host interleaved. The Ampere direct-RM profile therefore admits
-- a layout only with a video-memory USERD (nvidiaPlanHostLayoutAdmitted);
-- the UVM lifecycle's USERD is the last page of its video GPFIFO already.
-- System memory is one physically contiguous allocation; paged system
-- memory is not (NVOS32 PHYSICALITY NONCONTIGUOUS), which is what a buffer
-- too large for contiguous pages needs -- the GB10's arena, which has no
-- video memory to live in. The GPU reaches either through its page tables.
family NvidiaPlanHostMemory : Type 0
constructor NvidiaPlanHostSystemMemory
constructor NvidiaPlanHostVideoMemory
-- Noncontiguous physical pages, still host-cached and GPU virtually contiguous.
constructor NvidiaPlanHostPagedSystemMemory
-- Noncontiguous system memory the GPU caches in its L2, in 64 KiB pages,
-- never mapped into the process: the allocation cudaMalloc makes on the GB10
-- (read off the driver's RM calls, 2026-09-26: NV01_MEMORY_SYSTEM, attr
-- PAGE_SIZE_BIG | LOCATION_PCI | PHYSICALITY_NONCONTIGUOUS, attr2
-- GPU_CACHEABLE_YES | ZBC_PREFER_NO_ZBC, flags IGNORE_BANK_PLACEMENT |
-- MEMORY_HANDLE_PROVIDED | MAP_NOT_REQUIRED, PTE kind 6, 64 KiB aligned).
-- Paged system memory is not L2-cached by the GPU: an L2-resident copy runs
-- at 190 GB/s there against 880 GB/s here.
constructor NvidiaPlanHostGPUCachedSystemMemory
end-family
-- host 0 = not mapped into the process
family NvidiaPlanHostBuffer : Type 0
constructor NvidiaPlanHostBufferValue
field unrestricted nvidiaPlanHostBufferIdentity : Bytes
field unrestricted nvidiaPlanHostBufferGPU : Nat
field unrestricted nvidiaPlanHostBufferHost : Nat
field unrestricted nvidiaPlanHostBufferExtent : Nat
field unrestricted nvidiaPlanHostBufferMemory : (family NvidiaPlanHostMemory)
end-family
family NvidiaPlanHostBuffers : Type 0
constructor NvidiaPlanHostBuffersEnd
constructor NvidiaPlanHostBuffersNext
field unrestricted nvidiaPlanHostBuffersHead : (family NvidiaPlanHostBuffer)
recursive unrestricted nvidiaPlanHostBuffersTail
end-family
-- ---- the driver's interface (families) ----
-- These families and their functions live in PlanHost rather than a module
-- of their own: a module whose checks evaluate a layout's admission must
-- import the owner of every family that evaluation eliminates, and every
-- such module already imports PlanHost.
-- The NVIDIA kernel driver's ioctl interface, as far as a plan host encodes
-- it, and how a host chooses one at run time.
--
-- A plan host's escape and RM calls carry fixed structure layouts whose
-- sizes and field offsets belong to the driver's release branch, not to the
-- GPU: NVOS46 (the DMA map, its size encoded in the ioctl number) grew from
-- 56 to 64 bytes between the 570 and 580 branches, and the GPFIFO schedule
-- control parameters from 2 to 3 bytes. RunPod hosts of one card type run
-- different branches (sm_86 pods, 2026-09-24: 570.195, 580.65 .. 580.178,
-- 595.91), so an artifact names the branches it admits; the host asks the
-- running driver for its version (NV_ESC_CHECK_VERSION_STR,
-- PlanHost.phSelectDriverInterface) and runs the layout of the one branch
-- that version belongs to. A version no admitted branch names is refused by
-- name (`driver-branch`): a layout is never guessed from a neighbouring
-- branch. The GPU's own facts (classes, USERD placement, cache policy) stay
-- in PlanHost.NvidiaPlanHostABI.
--
-- The selection granularity is the branch (the version's major number): it
-- is the granularity at which these layouts change in NVIDIA's
-- open-gpu-kernel-modules (nvos.h, ctrla06c.h) and at which every recorded
-- run so far agreed. Each interface lists the exact versions it was
-- measured on; nvidiaDriverInterfaceAdmitted requires every one of them to
-- parse and to belong to the interface's branch, so evidence cannot be
-- attached to the wrong layout.
-- the exact driver versions a qualified run recorded
family NvidiaDriverVersions : Type 0
constructor NvidiaDriverVersionsEnd
constructor NvidiaDriverVersionsNext
field unrestricted nvidiaDriverVersionsHead : Bytes
recursive unrestricted nvidiaDriverVersionsTail
end-family
family NvidiaDriverInterface : Type 0
constructor NvidiaDriverInterfaceValue
-- the release branch: a version's major number (580 for 580.126.09)
field unrestricted nvidiaDriverInterfaceMajor : Nat
-- NV_ESC_RM_MAP_MEMORY_DMA's ioctl number (_IOWR('F', 0x57, NVOS46)): its
-- size field is the branch's NVOS46 size
field unrestricted nvidiaDriverInterfaceMapDMAIoctl : Nat
field unrestricted nvidiaDriverInterfaceNVOS46Size : Nat
field unrestricted nvidiaDriverInterfaceNVOS46DMAOffset : Nat
field unrestricted nvidiaDriverInterfaceNVOS46Status : Nat
-- the bytes of NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS; the wrong size is
-- NV_ERR_INVALID_ARGUMENT (0x1f), measured on an RTX A6000, 570.195.03
field unrestricted nvidiaDriverInterfaceScheduleParamsSize : Nat
-- the bytes of NV2080_CTRL_GPU_GET_NAME_STRING_PARAMS: the flags word and
-- the name, a union with a 64-entry unicode array through 580 (132), its
-- 64 ASCII bytes alone from 595 (68: ctrl2080gpu.h, 595.91.07); another
-- size is NV_ERR_INVALID_PARAM_STRUCT
field unrestricted nvidiaDriverInterfaceNameParamsSize : Nat
-- the driver versions a qualified run on this layout recorded, each NUL-free
field unrestricted nvidiaDriverInterfaceMeasured : (family NvidiaDriverVersions)
end-family
-- The branches an artifact admits, in the order the host tries them; at
-- least one by construction.
family NvidiaDriverInterfaces : Type 0
constructor NvidiaDriverInterfacesLast
field unrestricted nvidiaDriverInterfacesFinal : (family NvidiaDriverInterface)
constructor NvidiaDriverInterfacesNext
field unrestricted nvidiaDriverInterfacesHead : (family NvidiaDriverInterface)
recursive unrestricted nvidiaDriverInterfacesTail
end-family
-- ---- the version text ----
-- The driver answers NV_ESC_CHECK_VERSION_STR with its version as decimal
-- text, NUL-padded to 64 bytes: MAJOR "." MINOR ["." PATCH]. The parse is
-- the semantic statement of that format; nothing at run time depends on a
-- field after the major.
family NvidiaDriverVersion : Type 0
constructor NvidiaDriverVersionParsed
field unrestricted nvidiaDriverVersionMajor : Nat
field unrestricted nvidiaDriverVersionMinor : Nat
field unrestricted nvidiaDriverVersionPatch : Nat
-- the number of dot-separated fields: 2 or 3
field unrestricted nvidiaDriverVersionFields : Nat
constructor NvidiaDriverVersionMalformed
end-family
-- A left-to-right scan: every byte maps the scan state to the next one, by
-- naturals alone, so a refusal is a state (field 4) rather than a branch.
-- `field` is the field being read (0 major, 1 minor, 2 patch, 3 the NUL
-- padding, 4 refused); `digits` is that field's digit count, and in the
-- padding the number of fields the text had.
family NvidiaDriverVersionScan : Type 0
constructor NvidiaDriverVersionScanValue
field unrestricted nvidiaDriverVersionScanField : Nat
field unrestricted nvidiaDriverVersionScanDigits : Nat
field unrestricted nvidiaDriverVersionScanMajor : Nat
field unrestricted nvidiaDriverVersionScanMinor : Nat
field unrestricted nvidiaDriverVersionScanPatch : Nat
end-family
-- What a host assumes of the GPU and its driver. The driver's structure
-- layouts are per release branch (NvidiaDriverInterface, above):
-- an ABI admits one or more branches, the host asks the running driver for
-- its version before any card call, runs the layout of the branch that
-- version belongs to, and refuses any other version by name
-- (phSelectDriverInterface). The remaining fields are the GPU's.
family NvidiaPlanHostABI : Type 0
constructor NvidiaPlanHostABIValue
field unrestricted nvidiaPlanHostDrivers : (family NvidiaDriverInterfaces)
field unrestricted nvidiaPlanHostChannelClass : Nat
field unrestricted nvidiaPlanHostComputeClass : Nat
field unrestricted nvidiaPlanHostUsermodeClass : Nat
field unrestricted nvidiaPlanHostEngineType : Nat
-- Required location of a separately allocated direct-RM USERD buffer.
-- Discrete Ampere needs video memory; the measured integrated GB10 path
-- uses system memory. This is target policy, not a runtime retry choice.
field unrestricted nvidiaPlanHostDirectUSERDMemory : (family NvidiaPlanHostMemory)
field unrestricted nvidiaPlanHostDirectChannelFlags : Nat
-- Direct-RM cache snooping is target policy. The GB10 bring-up's host-cached
-- system buffers use 0x8010; the qualified Ampere path keeps 0x8000. See
-- Memory.ABI.memoryABIDMAMappingFlags. A CPU publication barrier alone does
-- not make a non-snooping GPU mapping coherent with cached CPU writes.
field unrestricted nvidiaPlanHostDirectDMAFlags : Nat
end-family
-- one upload: bytes, or the contents of a file at run time
family NvidiaPlanHostFills : Type 0
constructor NvidiaPlanHostFillsEnd
constructor NvidiaPlanHostFillBytes
field unrestricted nvidiaPlanHostFillHost : Nat
field unrestricted nvidiaPlanHostFillPayload : Bytes
recursive unrestricted nvidiaPlanHostFillsTail
constructor NvidiaPlanHostFillFile
field unrestricted nvidiaPlanHostFillFileHost : Nat
field unrestricted nvidiaPlanHostFillFilePath : Bytes
field unrestricted nvidiaPlanHostFillFileExtent : Nat
recursive unrestricted nvidiaPlanHostFillFileTail
end-family
-- one readback: a host range written to stdout after completion
family NvidiaPlanHostReads : Type 0
constructor NvidiaPlanHostReadsEnd
constructor NvidiaPlanHostReadsNext
field unrestricted nvidiaPlanHostReadHost : Nat
field unrestricted nvidiaPlanHostReadExtent : Nat
recursive unrestricted nvidiaPlanHostReadsTail
end-family
family NvidiaPlanHostLifecycle : Type 0
constructor NvidiaPlanHostDirectRM
-- the channel's GPFIFO entries (a power of two; the GPFIFO buffer holds them)
field unrestricted nvidiaPlanHostDirectRingEntries : Nat
constructor NvidiaPlanHostUVM
field unrestricted nvidiaPlanHostExternalRangeBase : Nat
field unrestricted nvidiaPlanHostExternalRangeExtent : Nat
end-family
-- How the host treats a driver status. Strict: every one is asserted zero
-- (the executables). Probe: every one after the root client's is recorded
-- and none asserted, so a host on a card reports which call refused instead
-- of stopping at it (the channel probe). The card-name and driver-branch
-- assertions hold in both: a probe against the wrong card, or a driver
-- whose ABI the host was not built for, stops.
family NvidiaPlanHostMode : Type 0
constructor NvidiaPlanHostStrict
constructor NvidiaPlanHostProbe
end-family
family NvidiaPlanHostLayout : Type 0
constructor NvidiaPlanHostLayoutValue
field unrestricted nvidiaPlanHostGPFIFO : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostPushbuffer : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostSemaphores : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostProgram : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostQMD : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostUSERD : (family NvidiaPlanHostBuffer)
field unrestricted nvidiaPlanHostData : (family NvidiaPlanHostBuffers)
field unrestricted nvidiaPlanHostABI : (family NvidiaPlanHostABI)
field unrestricted nvidiaPlanHostLifecycle : (family NvidiaPlanHostLifecycle)
field unrestricted nvidiaPlanHostExpectedName : Bytes
-- the host address the error notifier page is mapped at, 0 = not mapped
field unrestricted nvidiaPlanHostErrorHost : Nat
end-family
-- ---- the driver's interface: records, version text, selection statement ----
def nvidiaDriverMeasured =
(lambda unrestricted version : Bytes .
(lambda unrestricted rest : (family NvidiaDriverVersions) .
(constructor NvidiaDriverVersions NvidiaDriverVersionsNext version rest)))
def nvidiaDriverMeasuredEnd : (family NvidiaDriverVersions) =
(constructor NvidiaDriverVersions NvidiaDriverVersionsEnd)
-- The 570 branch: the 56-byte NVOS46 (_IOWR('F', 0x57, 56) = 0xC0384657,
-- dmaOffset at 40, status at 48) and the 2-byte schedule parameters
-- (bEnable, bSkipSubmit). Qualified on an RTX A6000, 570.195.03.
def nvidiaDriverInterface570 : (family NvidiaDriverInterface) =
(constructor NvidiaDriverInterface NvidiaDriverInterfaceValue
570 0xC0384657 56 40 48 2 132
(nvidiaDriverMeasured b"570.195.03" nvidiaDriverMeasuredEnd))
-- The 580 branch: the 64-byte NVOS46 (0xC0404657, dmaOffset at 48, status
-- at 56) and the 3-byte schedule parameters (bSkipEnable added). Qualified
-- on the RTX 3090 (580.178.04, 2026-09-24), the RTX 3070 and the H100 SXM
-- (580.126.09, comparisons/h100/README.md, 2026-10-10).
def nvidiaDriverInterface580 : (family NvidiaDriverInterface) =
(constructor NvidiaDriverInterface NvidiaDriverInterfaceValue
580 0xC0404657 64 48 56 3 132
(nvidiaDriverMeasured b"580.178.04" (nvidiaDriverMeasured b"580.126.09" nvidiaDriverMeasuredEnd)))
-- The 595 branch: the 580 branch's layouts but the name string's. NVIDIA's
-- open-gpu-kernel-modules
-- at 595.91.07 and 580.126.09 declare NVOS46_PARAMETERS and
-- NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS identically (nvos.h, ctrla06c.h), and
-- the escapes, channel, memory and class headers a plan host uses do not
-- differ (nv-ioctl.h, nv_escape.h, alloc_channel.h, cl0080/2080/90f1/a06c/
-- c86f/cbc0.h; read 2026-10-19). Qualified on the H100 SXM (595.91.07,
-- RunPod, 2026-10-19: the speedrun kernels' probes, bit for bit).
def nvidiaDriverInterface595 : (family NvidiaDriverInterface) =
(constructor NvidiaDriverInterface NvidiaDriverInterfaceValue
595 0xC0404657 64 48 56 3 68
(nvidiaDriverMeasured b"595.91.07" nvidiaDriverMeasuredEnd))
def nvidiaDriverInterfacesOne =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(constructor NvidiaDriverInterfaces NvidiaDriverInterfacesLast interface))
def nvidiaDriverInterfacesCons =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(lambda unrestricted rest : (family NvidiaDriverInterfaces) .
(constructor NvidiaDriverInterfaces NvidiaDriverInterfacesNext interface rest)))
-- ---- field access ----
def nvidiaDriverInterfaceMajorOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . major)))
def nvidiaDriverInterfaceMapDMAIoctlOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . mapDMA)))
def nvidiaDriverInterfaceNVOS46SizeOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . size)))
def nvidiaDriverInterfaceNVOS46DMAOffsetOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . dmaOffset)))
def nvidiaDriverInterfaceNVOS46StatusOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . status)))
def nvidiaDriverInterfaceScheduleParamsSizeOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . schedule)))
def nvidiaDriverInterfaceNameParamsSizeOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . name)))
def nvidiaDriverInterfaceMeasuredOf =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface
(lambda unrestricted current : (family NvidiaDriverInterface) . (family NvidiaDriverVersions)) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured . measured)))
-- the number of admitted branches
def nvidiaDriverInterfacesCount =
(lambda unrestricted interfaces : (family NvidiaDriverInterfaces) .
(eliminate NvidiaDriverInterfaces (lambda unrestricted current : (family NvidiaDriverInterfaces) . Nat) interfaces
(branch NvidiaDriverInterfacesLast final . 1)
(branch NvidiaDriverInterfacesNext head tail induction . (succ induction))))
-- the first admitted branch (what a fact true of every admitted branch, or
-- a single-branch artifact, reads)
def nvidiaDriverInterfacesFirst =
(lambda unrestricted interfaces : (family NvidiaDriverInterfaces) .
(eliminate NvidiaDriverInterfaces
(lambda unrestricted current : (family NvidiaDriverInterfaces) . (family NvidiaDriverInterface)) interfaces
(branch NvidiaDriverInterfacesLast final . final)
(branch NvidiaDriverInterfacesNext head tail induction . head)))
-- A major wider than this does not fit, with its dot, in the one word the
-- host compares (phSelectDriverInterface); no NVIDIA branch comes close.
def nvidiaDriverMajorDigitsMaximum : Nat =
7
def nvidiaDriverVersionRefused : Nat =
4
def nvidiaDriverVersionMalformedValue : (family NvidiaDriverVersion) =
(constructor NvidiaDriverVersion NvidiaDriverVersionMalformed)
def nvidiaDriverVersionScanStart : (family NvidiaDriverVersionScan) =
(constructor NvidiaDriverVersionScan NvidiaDriverVersionScanValue 0 0 0 0 0)
-- One byte. Each component of the next state is chosen by the same
-- byte class: a digit extends the current field (a major at most
-- nvidiaDriverMajorDigitsMaximum digits), a dot ends a nonempty major or
-- minor, the first NUL ends a nonempty minor or patch, a NUL in the padding
-- keeps it; anything else refuses, and a refusal is final.
def nvidiaDriverVersionStep =
(lambda unrestricted byte : Nat .
(lambda unrestricted scan : (family NvidiaDriverVersionScan) .
(eliminate NvidiaDriverVersionScan (lambda unrestricted current : (family NvidiaDriverVersionScan) . (family NvidiaDriverVersionScan)) scan
(branch NvidiaDriverVersionScanValue field digits major minor patch .
(let unrestricted digit = (naturalAnd (naturalLessOrEqual 48 byte) (naturalLessOrEqual byte 57)) in
(let unrestricted value = (naturalSaturatingSubtract byte 48) in
(let unrestricted reading = (naturalLess field 3) in
(let unrestricted extend =
(naturalAnd digit
(naturalAnd reading
(naturalOr (naturalNonzero field) (naturalLess digits nvidiaDriverMajorDigitsMaximum)))) in
(let unrestricted separate =
(naturalAnd (naturalEqual byte 46) (naturalAnd (naturalNonzero digits) (naturalLess field 2))) in
(let unrestricted terminate =
(naturalAnd (naturalEqual byte 0)
(naturalAnd (naturalNonzero digits) (naturalOr (naturalEqual field 1) (naturalEqual field 2)))) in
(let unrestricted pad = (naturalAnd (naturalEqual field 3) (naturalEqual byte 0)) in
(let unrestricted widened =
(lambda unrestricted which : Nat . (lambda unrestricted old : Nat .
(naturalSelect (naturalAnd extend (naturalEqual field which))
(naturalAdd (naturalMultiply old 10) value) old))) in
(constructor NvidiaDriverVersionScan NvidiaDriverVersionScanValue
(naturalSelect extend field
(naturalSelect separate (succ field)
(naturalSelect terminate 3
(naturalSelect pad 3 nvidiaDriverVersionRefused))))
(naturalSelect extend (succ digits)
(naturalSelect separate 0
(naturalSelect terminate (succ field) digits)))
(widened 0 major)
(widened 1 minor)
(widened 2 patch))))))))))))))
-- The end of the text: well formed when the padding began after two or three
-- fields, or the text ended without padding inside a nonempty minor or patch.
def nvidiaDriverVersionScanFinish =
(lambda unrestricted scan : (family NvidiaDriverVersionScan) .
(eliminate NvidiaDriverVersionScan (lambda unrestricted current : (family NvidiaDriverVersionScan) . (family NvidiaDriverVersion)) scan
(branch NvidiaDriverVersionScanValue field digits major minor patch .
(let unrestricted padded = (naturalAnd (naturalEqual field 3) (naturalAnd (naturalLessOrEqual 2 digits) (naturalLessOrEqual digits 3))) in
(let unrestricted unpadded = (naturalAnd (naturalNonzero digits) (naturalOr (naturalEqual field 1) (naturalEqual field 2))) in
(nat-eliminate (lambda unrestricted current : Nat . (family NvidiaDriverVersion))
nvidiaDriverVersionMalformedValue
(lambda unrestricted p : Nat . (lambda unrestricted ignored : (family NvidiaDriverVersion) .
(constructor NvidiaDriverVersion NvidiaDriverVersionParsed major minor patch
(naturalSelect padded digits (succ field)))))
(naturalOr padded unpadded)))))))
def nvidiaDriverVersionParse =
(lambda unrestricted text : Bytes .
(nvidiaDriverVersionScanFinish
(app
(bytes-eliminate
(lambda unrestricted current : Bytes .
(pi unrestricted state : (family NvidiaDriverVersionScan) . (family NvidiaDriverVersionScan)))
(lambda unrestricted state : (family NvidiaDriverVersionScan) . state)
(lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes .
(lambda unrestricted induction : (pi unrestricted state : (family NvidiaDriverVersionScan) . (family NvidiaDriverVersionScan)) .
(lambda unrestricted state : (family NvidiaDriverVersionScan) .
(induction (nvidiaDriverVersionStep (byte-to-nat head) state))))))
text)
nvidiaDriverVersionScanStart)))
-- the parsed major, or 0 for malformed text (no branch is 0)
def nvidiaDriverVersionMajorOf =
(lambda unrestricted text : Bytes .
(eliminate NvidiaDriverVersion (lambda unrestricted current : (family NvidiaDriverVersion) . Nat) (nvidiaDriverVersionParse text)
(branch NvidiaDriverVersionParsed major minor patch fields . major)
(branch NvidiaDriverVersionMalformed . 0)))
def nvidiaDriverVersionWellFormed =
(lambda unrestricted text : Bytes .
(eliminate NvidiaDriverVersion (lambda unrestricted current : (family NvidiaDriverVersion) . Nat) (nvidiaDriverVersionParse text)
(branch NvidiaDriverVersionParsed major minor patch fields . 1)
(branch NvidiaDriverVersionMalformed . 0)))
-- ---- what the host compares ----
-- A branch's prefix: its major's decimal digits and the dot ("580."). A
-- well-formed version begins with exactly one branch's prefix -- the dot
-- ends the major, so "580." never begins 5800.x -- which is how the host
-- selects with one word compare per admitted branch.
def nvidiaDriverMajorPrefix =
(lambda unrestricted major : Nat .
(bytes-append (naturalDecimalBytesWithin (naturalSaturatingSubtract nvidiaDriverMajorDigitsMaximum 1) major) b"."))
def nvidiaDriverInterfacePrefix =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(nvidiaDriverMajorPrefix (nvidiaDriverInterfaceMajorOf interface)))
-- little-endian: the word the prefix's bytes form at the start of an
-- otherwise zero 8-byte scratch
def nvidiaDriverTextWord =
(lambda unrestricted text : Bytes .
(bytes-eliminate
(lambda unrestricted current : Bytes . Nat)
0
(lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
(naturalAdd (byte-to-nat head) (naturalMultiply 256 induction)))))
text))
def nvidiaDriverInterfacePrefixWord =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(nvidiaDriverTextWord (nvidiaDriverInterfacePrefix interface)))
-- whether a version text begins with the branch's prefix: the host's test
def nvidiaDriverInterfaceMatches =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(lambda unrestricted text : Bytes .
(let unrestricted prefix = (nvidiaDriverInterfacePrefix interface) in
(bytes-equal (dataBytesTakeValidated (bytes-length prefix) text) prefix))))
-- The branch a version text selects: the 1-based position of the first
-- admitted branch it matches, 0 when none does (the host's refusal).
def nvidiaDriverInterfaceSelection =
(lambda unrestricted interfaces : (family NvidiaDriverInterfaces) .
(lambda unrestricted text : Bytes .
(eliminate NvidiaDriverInterfaces (lambda unrestricted current : (family NvidiaDriverInterfaces) . Nat) interfaces
(branch NvidiaDriverInterfacesLast final . (nvidiaDriverInterfaceMatches final text))
(branch NvidiaDriverInterfacesNext head tail induction .
(naturalSelect (nvidiaDriverInterfaceMatches head text) 1
(naturalSelect (naturalNonzero induction) (succ induction) 0))))))
-- ---- admission ----
-- An interface is admitted when its major fits the compared word, its
-- NVOS46 fields lie inside the structure (the status word too), and every
-- version it was measured on parses and belongs to its branch.
def nvidiaDriverVersionsBelong =
(lambda unrestricted major : Nat .
(lambda unrestricted versions : (family NvidiaDriverVersions) .
(eliminate NvidiaDriverVersions (lambda unrestricted current : (family NvidiaDriverVersions) . Nat) versions
(branch NvidiaDriverVersionsEnd . 1)
(branch NvidiaDriverVersionsNext head tail induction .
(naturalAnd (naturalEqual (nvidiaDriverVersionMajorOf head) major) induction)))))
def nvidiaDriverVersionsNonempty =
(lambda unrestricted versions : (family NvidiaDriverVersions) .
(eliminate NvidiaDriverVersions (lambda unrestricted current : (family NvidiaDriverVersions) . Nat) versions
(branch NvidiaDriverVersionsEnd . 0)
(branch NvidiaDriverVersionsNext head tail induction . 1)))
def nvidiaDriverInterfaceAdmitted =
(lambda unrestricted interface : (family NvidiaDriverInterface) .
(eliminate NvidiaDriverInterface (lambda unrestricted current : (family NvidiaDriverInterface) . Nat) interface
(branch NvidiaDriverInterfaceValue major mapDMA size dmaOffset status schedule name measured .
(naturalAnd (naturalNonzero major)
(naturalAnd (naturalLessOrEqual (bytes-length (nvidiaDriverMajorPrefix major)) 8)
(naturalAnd (naturalLessOrEqual (naturalAdd dmaOffset 8) size)
(naturalAnd (naturalLessOrEqual (naturalAdd status 4) size)
(naturalAnd (naturalNonzero schedule)
(naturalAnd (naturalLessOrEqual 68 name)
(naturalAnd (nvidiaDriverVersionsNonempty measured)
(nvidiaDriverVersionsBelong major measured)))))))))))
-- whether `major` is the branch of an interface in `interfaces`
def nvidiaDriverInterfacesHaveMajor =
(lambda unrestricted major : Nat .
(lambda unrestricted interfaces : (family NvidiaDriverInterfaces) .
(eliminate NvidiaDriverInterfaces (lambda unrestricted current : (family NvidiaDriverInterfaces) . Nat) interfaces
(branch NvidiaDriverInterfacesLast final . (naturalEqual (nvidiaDriverInterfaceMajorOf final) major))
(branch NvidiaDriverInterfacesNext head tail induction .
(naturalOr (naturalEqual (nvidiaDriverInterfaceMajorOf head) major) induction)))))
-- Every admitted branch admitted, and no branch twice: two layouts for one
-- branch would make the selection depend on their order.
def nvidiaDriverInterfacesAdmitted =
(lambda unrestricted interfaces : (family NvidiaDriverInterfaces) .
(eliminate NvidiaDriverInterfaces (lambda unrestricted current : (family NvidiaDriverInterfaces) . Nat) interfaces
(branch NvidiaDriverInterfacesLast final . (nvidiaDriverInterfaceAdmitted final))
(branch NvidiaDriverInterfacesNext head tail induction .
(naturalAnd (nvidiaDriverInterfaceAdmitted head)
(naturalAnd (naturalIsZero (nvidiaDriverInterfacesHaveMajor (nvidiaDriverInterfaceMajorOf head) tail))
induction)))))
-- Discrete Ampere (GA10x): AMPERE_CHANNEL_GPFIFO_A 0xC56F, AMPERE_COMPUTE_B
-- 0xC7C0, AMPERE_USERMODE_A 0xC561, USERD in video memory. The branch is the
-- layout the host runs; the 575 branch (the RTX 3070 fixtures' retired ABI)
-- is no longer offered for any sm_86 card on RunPod (2026-09-24: 570.195,
-- 580.65 .. 580.178, 595.91), so it could not be qualified again and is not
-- an interface; 595 has never been measured and is refused.
def nvidiaPlanHostAmpereOn =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(constructor NvidiaPlanHostABI NvidiaPlanHostABIValue drivers 0xC56F 0xC7C0 0xC561 0
(constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000))
def nvidiaPlanHostAmpere570 : (family NvidiaPlanHostABI) =
(nvidiaPlanHostAmpereOn (nvidiaDriverInterfacesOne nvidiaDriverInterface570))
def nvidiaPlanHostAmpere580 : (family NvidiaPlanHostABI) =
(nvidiaPlanHostAmpereOn (nvidiaDriverInterfacesOne nvidiaDriverInterface580))
-- An Ampere host that runs on either measured branch, whichever the pod's
-- driver is.
def nvidiaPlanHostAmpere : (family NvidiaPlanHostABI) =
(nvidiaPlanHostAmpereOn
(nvidiaDriverInterfacesCons nvidiaDriverInterface580 (nvidiaDriverInterfacesOne nvidiaDriverInterface570)))
-- The H100 SXM (compute 9.0): Hopper's classes (open-gpu-doc /
-- open-gpu-kernel-modules clc86f.h, clcbc0.h, clc661.h):
-- HOPPER_CHANNEL_GPFIFO_A 0xC86F, HOPPER_COMPUTE_A 0xCBC0, HOPPER_USERMODE_A
-- 0xC661. Discrete, so USERD stays in video memory as on Ampere. Driver
-- 580.126.09 on RunPod, 2026-10-10, on the 580 interface.
def nvidiaPlanHostHopperOn =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(constructor NvidiaPlanHostABI NvidiaPlanHostABIValue drivers 0xC86F 0xCBC0 0xC661 0
(constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000))
def nvidiaPlanHostHopper580 : (family NvidiaPlanHostABI) =
(nvidiaPlanHostHopperOn (nvidiaDriverInterfacesOne nvidiaDriverInterface580))
-- The H100 on RunPod's current branches: 595 (hosts moved to it from 580
-- underneath a running pod, 2026-10-19), then 580.
def nvidiaPlanHostHopperRunPod : (family NvidiaPlanHostABI) =
(nvidiaPlanHostHopperOn
(nvidiaDriverInterfacesCons nvidiaDriverInterface595 (nvidiaDriverInterfacesOne nvidiaDriverInterface580)))
-- Hopper on either branch. The 570 layout is the driver's, measured on an
-- RTX A6000 (570.195.03); Hopper's classes are unchanged across branches.
-- No H100 on a 570 driver has run yet: that pod is the first device run of
-- this ABI's 570 half (docs/PLAN-NANOCHAT-SPEEDRUN.md, W4).
def nvidiaPlanHostHopper : (family NvidiaPlanHostABI) =
(nvidiaPlanHostHopperOn
(nvidiaDriverInterfacesCons nvidiaDriverInterface580 (nvidiaDriverInterfacesOne nvidiaDriverInterface570)))
-- The DGX Spark's GB10 (compute 12.1) on the 580 branch: the classes this
-- GPU's class list offers and the ladder allocated (tools/dgx/rung_tsg.py,
-- rung_execute.py): BLACKWELL_CHANNEL_GPFIFO_A 0xC96F, BLACKWELL_COMPUTE_B
-- 0xCEC0, HOPPER_USERMODE_A 0xC661.
def nvidiaPlanHostBlackwell580 : (family NvidiaPlanHostABI) =
(constructor
NvidiaPlanHostABI
NvidiaPlanHostABIValue
(nvidiaDriverInterfacesOne nvidiaDriverInterface580)
0xC96F
0xCEC0
0xC661
0
-- USERD in system memory (the GB10's channel buffers, Coppelius.Build.
-- NativeHost), the channel flags every UVM plan allocates with, and the
-- direct-RM DMA flags, which a UVM plan never reads
(constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)
0x01000000
0x8000)
-- A layout built for another driver ABI: every buffer, the lifecycle and
-- the expected card unchanged, only the ABI (the DMA-map parameters, the
-- classes, the driver branch it demands) replaced.
def nvidiaPlanHostWithABI =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family NvidiaPlanHostLayout))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
previous
lifecycle
expectedName
errorHost
.
(constructor
NvidiaPlanHostLayout
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost)))))
-- Preserve existing data-buffer ordinals when adding a separate residency.
-- Host request plans use those ordinals to locate staging, so prepending an
-- allocation would redirect valid requests to the wrong buffer. Admission
-- still checks the resulting mappings, bounds and allocation count.
def nvidiaPlanHostBuffersConcat =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted suffix : (family NvidiaPlanHostBuffers) .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) .
(family NvidiaPlanHostBuffers))
buffers
(branch NvidiaPlanHostBuffersEnd . suffix)
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext head induction)))))
def nvidiaPlanHostBuffersAppend =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(nvidiaPlanHostBuffersConcat
buffers
(constructor
NvidiaPlanHostBuffers
NvidiaPlanHostBuffersNext
buffer
(constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd)))))
def nvidiaPlanHostAppendDataBuffers =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family NvidiaPlanHostLayout))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(constructor
NvidiaPlanHostLayout
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
(nvidiaPlanHostBuffersConcat data buffers)
abi
lifecycle
expectedName
errorHost)))))
def nvidiaPlanHostAppendDataBuffer =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(nvidiaPlanHostAppendDataBuffers
layout
(constructor
NvidiaPlanHostBuffers
NvidiaPlanHostBuffersNext
buffer
(constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd)))))
-- ---- operands and commands ----
def phWord =
(lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))
def phImm =
nativeLaunchRecipeImmediate
def phSlot =
nativeLaunchRecipeSlotValue
def phStore =
nativeLaunchRecipeStore
def phDiscard : (family NativePhysicalResultBinding) =
(constructor NativePhysicalResultBinding NativePhysicalDiscardResult)
def phState =
(lambda unrestricted offset : Nat .
(constructor NativePhysicalOperand NativePhysicalStateAddress (phWord offset)))
def phLoad =
(lambda unrestricted offset : Nat .
(constructor NativePhysicalOperand NativePhysicalStateLoad64 (phWord offset)))
def phPayload : (family NativePhysicalOperand) =
(constructor NativePhysicalOperand NativePhysicalPayloadAddress modelWord64Zero)
def phArgs =
(lambda unrestricted a0 : (family NativePhysicalOperand) .
(lambda unrestricted a1 : (family NativePhysicalOperand) .
(lambda unrestricted a2 : (family NativePhysicalOperand) .
(lambda unrestricted a3 : (family NativePhysicalOperand) .
(lambda unrestricted a4 : (family NativePhysicalOperand) .
(lambda unrestricted a5 : (family NativePhysicalOperand) .
(constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5)))))))
def phArgs3 =
(lambda unrestricted a0 : (family NativePhysicalOperand) .
(lambda unrestricted a1 : (family NativePhysicalOperand) .
(lambda unrestricted a2 : (family NativePhysicalOperand) .
(phArgs a0 a1 a2 (phImm 0) (phImm 0) (phImm 0)))))
def phIdentity : Bytes =
b"nvidia-plan-host"
def phNext =
(lambda unrestricted operation : (family NativePhysicalOperation) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nativeLaunchRecipeCommand operation phIdentity tail)))
def phCall =
(lambda unrestricted number : Nat .
(lambda unrestricted argv : (family NativePhysicalArguments) .
(lambda unrestricted payload : Bytes .
(lambda unrestricted result : (family NativePhysicalResultBinding) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor
NativePhysicalOperation
NativePhysicalSystemCall
(phImm number)
argv
payload
result)
tail))))))
def phCopy =
(lambda unrestricted offset : Nat .
(lambda unrestricted payload : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor
NativePhysicalOperation
NativePhysicalCopyPayloadToState
(phWord offset)
(phWord (bytes-length payload))
payload)
tail))))
-- Linux x86-64
def phSysRead : Nat =
0
def phSysWrite : Nat =
1
def phSysClose : Nat =
3
def phSysFstat : Nat =
5
def phSysFsync : Nat =
74
def phSysMmap : Nat =
9
def phSysIoctl : Nat =
16
def phSysDup2 : Nat =
33
def phSysExitGroup : Nat =
231
def phSysOpenat : Nat =
257
def phSysPipe2 : Nat =
293
def phAtFdCwd : Nat =
18446744073709551516
def phOpenFlags : Nat =
0x80002
def phMapAnonymousFixed : Nat =
0x32
def phMapSharedFixed : Nat =
0x11
def phNoDescriptor : Nat =
18446744073709551615
-- RM and UVM escapes
def phRMAlloc : Nat =
0xC020462B
def phRMControl : Nat =
0xC020462A
def phRMMapMemory : Nat =
0xC038464E
def phRMFree : Nat =
0xC0104629
def phRegisterFD : Nat =
0xC00446C9
def phWaitOpen : Nat =
0xC00846DA
def phUVMInitialize : Nat =
0x30000001
def phUVMMMInitialize : Nat =
75
def phUVMRegisterGPU : Nat =
37
def phUVMRegisterGPUVASpace : Nat =
25
def phUVMRegisterChannel : Nat =
27
def phUVMCreateExternalRange : Nat =
73
def phUVMMapExternalAllocation : Nat =
33
def phUVMChannelRangeBase : Nat =
0xA00000000
def phUVMChannelRangeExtent : Nat =
0x4000000
-- result slots and fixed descriptors
def phSlotControl : Nat =
0
def phSlotGPU : Nat =
1
def phSlotMap : Nat =
2
def phSlotFile : Nat =
3
-- slots 4..13 belong to the request host (PlanHostRequest), 14 and 15 to
-- the native telemetry. Transfers own the next slot and never overwrite a
-- request file descriptor or a mapping result while checking short I/O. The
-- recorder borrows that transfer slot for its directory only after its final
-- pipe fill; it closes the directory before allowing the continuation to run.
def phSlotTransfer : Nat =
16
def phSlots : Nat =
(succ phSlotTransfer)
def phFdControl : Nat =
100
def phFdCardS = (lambda unrestricted session : Nat . (naturalSelect (naturalIsZero session) 101 (naturalAdd 120 session)))
def phFdCard : Nat =
(phFdCardS 0)
def phFdMap : Nat =
102
def phFdUVM : Nat =
103
def phFdUVMMemoryMap : Nat =
104
-- ---- sessions: more than one card in one process ----
-- Session 0 is the one card a host has always driven, with every handle,
-- descriptor and address it always had (each definition below is its
-- `S` form at session 0). A session s > 0 is another card the same
-- process drives (docs/PRD-8XH100-ON-A-BUDGET.md F4): its RM handles
-- offset by s 0x100000 in the one RM client, its card on descriptor
-- 120 + s, its doorbell 64 KiB s after session 0's, its work-submit
-- token 16 s bytes after. The client, the control descriptor, the
-- parameter page and the state are shared: sessions come up one after
-- another, and every call block is consumed by its own ioctl.
def phSessionHandle = (lambda unrestricted session : Nat . (lambda unrestricted handle : Nat .
(naturalAdd handle (naturalMultiply session 0x100000))))
-- RM handles, caller-chosen for children
def phHDeviceS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD0080))
def phHDevice : Nat =
(phHDeviceS 0)
def phHSubdeviceS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD2080))
def phHSubdevice : Nat =
(phHSubdeviceS 0)
def phHVASpaceS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD90F1))
def phHVASpace : Nat =
(phHVASpaceS 0)
def phHErrorS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD0E44))
def phHError : Nat =
(phHErrorS 0)
def phHGroupS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEADA06C))
def phHGroup : Nat =
(phHGroupS 0)
def phHContextS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD9067))
def phHContext : Nat =
(phHContextS 0)
def phHDMAS = (lambda unrestricted session : Nat . (phSessionHandle session 0xDEAD0070))
def phHDMA : Nat =
(phHDMAS 0)
def phHMemoryS = (lambda unrestricted session : Nat . (lambda unrestricted index : Nat . (phSessionHandle session (naturalAdd 0xB0000000 index))))
def phHMemory =
(phHMemoryS 0)
def phHVirtualS = (lambda unrestricted session : Nat . (lambda unrestricted index : Nat . (phSessionHandle session (naturalAdd 0xB1000000 index))))
def phHVirtual =
(phHVirtualS 0)
def phHClassS = (lambda unrestricted session : Nat . (lambda unrestricted class : Nat . (phSessionHandle session (naturalAdd 0xDEAD0000 class))))
def phHClass =
(phHClassS 0)
-- state layout, 16 KiB: RM call blocks, then a 16-byte status record per
-- buffer, then 256 bytes of call blocks per buffer (at most 24 buffers, to
-- 10240); the request host's areas follow (PlanHostRequest)
def phStateExtent : Nat =
16384
def phBufferBlocksEnd : Nat =
10240
def phRoot : Nat =
0
def phDev : Nat =
64
def phSub : Nat =
128
def phVAS : Nat =
192
def phErrMap : Nat =
256
def phErr : Nat =
2048
def phGroup : Nat =
2112
def phCtx : Nat =
2176
def phChan : Nat =
2240
def phComp : Nat =
2304
def phUser : Nat =
2368
def phBind : Nat =
2432
def phSched : Nat =
2496
def phTok : Nat =
2560
def phDoorMap : Nat =
2624
def phWait : Nat =
2688
def phPipe : Nat =
2752
def phScratch : Nat =
2816
def phName : Nat =
2880
def phPreempt : Nat =
3008
def phFree : Nat =
3040
def phDMAObject : Nat =
3072
def phUVMControl : Nat =
3136
def phBufferState =
(lambda unrestricted index : Nat . (naturalAdd 4096 (naturalMultiply index 256)))
def phBufferStatus =
(lambda unrestricted index : Nat . (naturalAdd 3200 (naturalMultiply index 16)))
def phBuffersMaximum : Nat =
24
-- the fixed anonymous parameter page, 64 KiB
-- Extent of the maintained parameter mapping used by the native session.
-- Allocation accounting and the mmap command must use this same owner.
def nvidiaPlanHostParameterMappingBytes : Nat =
0x10000
def phParams : Nat =
0x50000000
def phDevP : Nat =
0x50000000
def phSubP : Nat =
0x50000100
def phVASP : Nat =
0x50000200
def phErrP : Nat =
0x50001100
def phGroupP : Nat =
0x50001200
def phCtxP : Nat =
0x50001300
def phChanP : Nat =
0x50001400
def phBindP : Nat =
0x50001600
def phSchedP : Nat =
0x50001700
def phTokPS = (lambda unrestricted session : Nat . (naturalAdd 0x50001800 (naturalMultiply session 16)))
def phTokP : Nat =
(phTokPS 0)
def phRegFdP : Nat =
0x50001980
def phPreemptP : Nat =
0x50001A00
def phNameP : Nat =
0x50001B00
def phMemP =
(lambda unrestricted index : Nat . (naturalAdd 0x50002000 (naturalMultiply index 0x200)))
def phVirtP =
(lambda unrestricted index : Nat . (naturalAdd 0x50002100 (naturalMultiply index 0x200)))
def phDMAObjectP : Nat =
0x50007F00
def phUVMGidP : Nat =
0x50008000
def phUVMInitP : Nat =
0x50008200
def phUVMMMP : Nat =
0x50008300
def phUVMRegisterGPUP : Nat =
0x50008400
def phUVMRegisterVASpaceP : Nat =
0x50008500
def phUVMRegisterChannelP : Nat =
0x50008600
def phUVMCreateRangeP : Nat =
0x50008700
def phUVMMapAllocationP : Nat =
0x50009000
def phDoorHostS = (lambda unrestricted session : Nat . (naturalAdd 0x60800000 (naturalMultiply session 0x10000)))
def phDoorHost : Nat =
(phDoorHostS 0)
def phStatusSentinel : Nat =
0xFFFFFFFF
-- ---- little-endian blocks ----
def phZeros =
(lambda unrestricted count : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
b""
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
count))
def phDrop =
dataBytesDropValidated
def phTake =
dataBytesTakeValidated
def phW32 =
(lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value)))
def phW64 =
(lambda unrestricted value : Nat . (dataBytesWord64LE (phWord value)))
def phSet =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted field : Bytes .
(bytes-append
(phTake offset block)
(bytes-append field (phDrop (naturalAdd offset (bytes-length field)) block))))))
def phSet32 =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted value : Nat . (phSet block offset (phW32 value)))))
def phSet64 =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted value : Nat . (phSet block offset (phW64 value)))))
-- ---- the pipe memcpy ----
def phCopyStateToState =
(lambda unrestricted destination : Nat .
(lambda unrestricted source : Nat .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysWrite
(phArgs3 (phLoad (naturalAdd phPipe 4)) (phState source) (phImm count))
b""
phDiscard
(phCall
phSysRead
(phArgs3 (phLoad phPipe) (phState destination) (phImm count))
b""
phDiscard
tail))))))
-- A pipe is not an unbounded staging buffer. A single-threaded write/read
-- pair deadlocks when its write exceeds capacity (the matrix qualification
-- stopped in write(901120), after filling 65536 bytes). Drain every bounded
-- chunk before writing another. Linux PIPE_BUF is 4096 on both target ABIs;
-- the empty pipe admits that atomic extent even when capacity is one page.
-- Short/error returns fail by name, including interruption; no partial copy
-- is reported as a successful upload. Result slot ownership is explicit.
def phPipeChunkBytes : Nat =
4096
def phPipeChunkCount =
(lambda unrestricted count : Nat .
(naturalAdd
(naturalDivideUnchecked count phPipeChunkBytes)
(naturalNonzero (naturalModuloUnchecked count phPipeChunkBytes))))
def phPipeChunk =
(lambda unrestricted source : (family NativePhysicalOperand) .
(lambda unrestricted destination : (family NativePhysicalOperand) .
(lambda unrestricted count : Nat .
(lambda unrestricted payload : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysWrite
(phArgs3 (phLoad (naturalAdd phPipe 4)) source (phImm count))
payload
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm count)
b"pipe-copy-write"
(phCall
phSysRead
(phArgs3 (phLoad phPipe) destination (phImm count))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm count)
b"pipe-copy-read"
tail)))))))))
def phFill =
(lambda unrestricted address : Nat .
(lambda unrestricted payload : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(nat-eliminate
(lambda unrestricted remaining : Nat .
(pi unrestricted at : Nat .
(pi unrestricted bytes : Bytes . (family NativePhysicalCommands))))
(lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . tail))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))) .
(lambda unrestricted at : Nat .
(lambda unrestricted bytes : Bytes .
(let unrestricted count =
(naturalMinimum phPipeChunkBytes (bytes-length bytes))
in
(phPipeChunk
phPayload
(phImm at)
count
(dataBytesTakeValidated count bytes)
(induction (naturalAdd at count) (dataBytesDropValidated count bytes))))))))
(phPipeChunkCount (bytes-length payload)))
address
payload))))
-- Address-based copies share the same transfer/check mechanism. Their
-- ranges must be disjoint as before; this is not an overlapping memmove.
def phPipeRanges =
(lambda unrestricted source : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
(lambda unrestricted destination : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted chunks =
(phPipeChunkCount count)
in
(nat-eliminate
(lambda unrestricted i : Nat . (family NativePhysicalCommands))
tail
(lambda unrestricted index : Nat .
(lambda unrestricted rest : (family NativePhysicalCommands) .
(let unrestricted offset =
(naturalMultiply
(naturalSaturatingSubtract chunks (succ index))
phPipeChunkBytes)
in
(phPipeChunk
(source offset)
(destination offset)
(naturalMinimum phPipeChunkBytes (naturalSaturatingSubtract count offset))
b""
rest))))
chunks))))))
def phCopyMappedToState =
(lambda unrestricted address : Nat .
(lambda unrestricted destination : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phImm (naturalAdd address offset)))
(lambda unrestricted offset : Nat . (phState (naturalAdd destination offset))))))
def phCopyStateToMapped =
(lambda unrestricted source : Nat .
(lambda unrestricted address : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phState (naturalAdd source offset)))
(lambda unrestricted offset : Nat . (phImm (naturalAdd address offset))))))
def phCopyMappedToMapped =
(lambda unrestricted source : Nat .
(lambda unrestricted destination : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phImm (naturalAdd source offset)))
(lambda unrestricted offset : Nat . (phImm (naturalAdd destination offset))))))
-- the pipe the memcpys above go through; every entry point creates it first
def phPipeCreate =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall phSysPipe2 (phArgs3 (phState phPipe) (phImm 0) (phImm 0)) b"" phDiscard tail))
-- Read the declared prefix into a mapped buffer. Short reads (including
-- interruption), missing files and I/O errors fail before later uploads or
-- submissions; an unread suffix is allowed by this fill's prefix contract.
-- Keep the descriptor in phScratch while phSlotFile carries read/close
-- results. Both are owned temporaries across this straight-line fragment;
-- no caller's request or telemetry slot is borrowed. Closing also prevents
-- a multi-tensor import from exhausting the process's file descriptors.
-- Bytes has an explicit extent; openat requires a terminating zero. An
-- eight-byte path otherwise runs into the next payload in the host image.
-- Caller-supplied trailing zeros remain harmless; never rely on pool padding.
-- The descriptor in phScratch read into `address`, `count` bytes, a chunk
-- of at most 2^30 bytes a read: Linux returns at most 0x7ffff000 bytes from
-- one read, so a larger file (a record-size probe's 2 GiB of logits) takes
-- several; each must return its whole chunk.
def phReadChunkBytes : Nat = (naturalPowerOfTwo 30)
def phReadChunks =
(lambda unrestricted address : Nat .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(nat-eliminate (lambda unrestricted n : Nat . (pi unrestricted k : Nat . (family NativePhysicalCommands)))
(lambda unrestricted k : Nat . tail)
(lambda unrestricted p : Nat . (lambda unrestricted rest : (pi unrestricted k : Nat . (family NativePhysicalCommands)) .
(lambda unrestricted k : Nat .
(let unrestricted start = (naturalMultiply k phReadChunkBytes) in
(let unrestricted left = (naturalSaturatingSubtract count start) in
(let unrestricted chunk = (naturalSelect (naturalLess left phReadChunkBytes) left phReadChunkBytes) in
(phCall
phSysRead
(phArgs3 (phLoad phScratch) (phImm (naturalAdd address start)) (phImm chunk))
b""
(phStore phSlotFile)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotFile)
(phImm chunk)
b"input-file-read"
(rest (succ k))))))))))
(let unrestricted chunks = (naturalDivideUnchecked (naturalAdd count (naturalSaturatingSubtract phReadChunkBytes 1)) phReadChunkBytes) in
(naturalSelect (naturalIsZero chunks) 1 chunks)))
0))))
def phReadFile =
(lambda unrestricted path : Bytes .
(lambda unrestricted address : Nat .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm 0))
(bytes-append path b"\x00")
(phStore phSlotFile)
(phNext
(constructor
NativePhysicalOperation
NativePhysicalStoreWord64
(phState phScratch)
(phSlot phSlotFile))
(phReadChunks address count
(phCall
phSysClose
(phArgs3 (phLoad phScratch) (phImm 0) (phImm 0))
b""
(phStore phSlotFile)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotFile)
(phImm 0)
b"input-file-close"
tail)))))))))
def phRangeBase =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM entries . 0)
(branch NvidiaPlanHostUVM base extent . base)))
def phRangeExtent =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM entries . 0)
(branch NvidiaPlanHostUVM base extent . extent)))
-- 1 when the buffer lies inside the lifecycle's pre-created external range,
-- the video arena: such a buffer is mapped into the range, not given one
def phInsideRange =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted gpu : Nat .
(lambda unrestricted extent : Nat .
(naturalAnd
(naturalNonzero (phRangeExtent lifecycle))
(naturalAnd
(naturalLessOrEqual (phRangeBase lifecycle) gpu)
(naturalLessOrEqual
(naturalAdd gpu extent)
(naturalAdd (phRangeBase lifecycle) (phRangeExtent lifecycle))))))))
def phWhen =
(lambda unrestricted flag : Nat .
(lambda unrestricted commands : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nat-eliminate
(lambda unrestricted current : Nat . (family NativePhysicalCommands))
tail
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (family NativePhysicalCommands) . (commands tail)))
flag))))
-- ---- fail closed ----
def phAssertStateZero32 =
(lambda unrestricted identity : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
phScratch
(phZeros 8)
(phCopyStateToState
phScratch
offset
4
(nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
def phAssertMappedZero32 =
(lambda unrestricted identity : Bytes .
(lambda unrestricted address : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
phScratch
(phZeros 8)
(phCopyMappedToState
address
phScratch
4
(nativeLaunchRecipeAssertEqual (phLoad phScratch) (phImm 0) identity tail))))))
-- the same, unless tolerated
def phCheckStateZero32 =
(lambda unrestricted identity : Bytes .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phWhen (naturalIsZero tolerate) (phAssertStateZero32 identity offset) tail)))))
def phCheckMappedZero32 =
(lambda unrestricted identity : Bytes .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted address : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phWhen (naturalIsZero tolerate) (phAssertMappedZero32 identity address) tail)))))
-- ---- RM alloc / control, each asserted ----
-- Parent/object 0 denotes the root client returned by RM. Child handles are
-- explicit; the root handle is copied at runtime, never guessed or replayed.
def phAlloc =
(lambda unrestricted identity : Bytes .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted block : Nat .
(lambda unrestricted parent : Nat .
(lambda unrestricted class : Nat .
(lambda unrestricted paramsAddress : Nat .
(lambda unrestricted paramsSize : Nat .
(lambda unrestricted handle : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
block
(phSet32
(phSet32
(phSet32
(phSet32 (phSet32 (phSet32 (phZeros 32) 4 parent) 8 handle) 12 class)
16
paramsAddress)
24
paramsSize)
28
phStatusSentinel)
(phCopyStateToState
block
(naturalAdd phRoot 8)
4
(phWhen
(naturalIsZero parent)
(phCopyStateToState (naturalAdd block 4) (naturalAdd phRoot 8) 4)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState block))
b""
phDiscard
(phCopyStateToState
statusOffset
(naturalAdd block 28)
4
(phCheckStateZero32 identity tolerate (naturalAdd block 28) tail))))))))))))))))
def phControl =
(lambda unrestricted identity : Bytes .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted block : Nat .
(lambda unrestricted object : Nat .
(lambda unrestricted command : Nat .
(lambda unrestricted paramsAddress : Nat .
(lambda unrestricted paramsSize : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
block
(phSet32
(phSet32
(phSet32
(phSet32 (phSet32 (phZeros 32) 4 object) 8 command)
16
paramsAddress)
24
paramsSize)
28
phStatusSentinel)
(phCopyStateToState
block
(naturalAdd phRoot 8)
4
(phWhen
(naturalIsZero object)
(phCopyStateToState (naturalAdd block 4) (naturalAdd phRoot 8) 4)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm phRMControl) (phState block))
b""
phDiscard
(phCopyStateToState
statusOffset
(naturalAdd block 28)
4
(phCheckStateZero32 identity tolerate (naturalAdd block 28) tail)))))))))))))))
-- a UVM ioctl whose status word lives in its parameter block: the word is
-- recorded in the UVM status record, one 4-byte slot per call, and asserted
-- zero unless the call is one the proven hosts tolerate a non-zero from
def phUVMStatusRecord : Nat =
3584
def phUVMStatusSlot =
(lambda unrestricted slot : Nat . (naturalAdd phUVMStatusRecord (naturalMultiply slot 4)))
def phUVMStatusRecordExtent : Nat =
512
-- RM status record slots after the UVM slots
def phRMStatusSlot =
(lambda unrestricted slot : Nat . (naturalAdd 4000 (naturalMultiply slot 4)))
-- the `tolerate` an RM alloc or control takes under a mode
def phTolerate =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(eliminate
NvidiaPlanHostMode
(lambda unrestricted current : (family NvidiaPlanHostMode) . Nat)
mode
(branch NvidiaPlanHostStrict . 0)
(branch NvidiaPlanHostProbe . 1)))
def phUVMCall =
(lambda unrestricted identity : Bytes .
(lambda unrestricted slot : Nat .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted descriptor : Nat .
(lambda unrestricted request : Nat .
(lambda unrestricted paramsAddress : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysIoctl
(phArgs3 (phImm descriptor) (phImm request) (phImm paramsAddress))
b""
phDiscard
(phCopyMappedToState
(naturalAdd paramsAddress statusOffset)
(phUVMStatusSlot slot)
4
(phCheckMappedZero32
identity
tolerate
(naturalAdd paramsAddress statusOffset)
tail)))))))))))
-- the same, right after the UVM device was opened onto `descriptor`: the
-- dup2 that placed it returned `descriptor` (it returns a negative errno
-- when the open failed), or -- unless `openTolerate` -- the host stops with
-- `uvm-open`, not at the ioctl that finds no device behind the descriptor.
-- Measured on RunPod, 2026-09-24: a container whose /dev/nvidia-uvm exists
-- but opens with EIO used to stop at `uvm-initialize`.
def phUVMCallAfterOpen =
(lambda unrestricted openTolerate : Nat .
(lambda unrestricted identity : Bytes .
(lambda unrestricted slot : Nat .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted descriptor : Nat .
(lambda unrestricted request : Nat .
(lambda unrestricted paramsAddress : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phWhen
(naturalIsZero openTolerate)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotMap)
(phImm descriptor)
b"uvm-open")
(phUVMCall
identity
slot
tolerate
descriptor
request
paramsAddress
statusOffset
tail)))))))))))
-- ---- buffers ----
-- Preserve the layout's semantic buffer name at the RM allocation boundary.
-- A generic allocation error hides which resource the driver refused.
def phBufferIdentity =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Bytes)
buffer
(branch NvidiaPlanHostBufferValue identity gpu host extent memory . identity)))
def phBufferGPU =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch NvidiaPlanHostBufferValue identity gpu host extent memory . gpu)))
def phBufferHost =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch NvidiaPlanHostBufferValue identity gpu host extent memory . host)))
def phBufferExtent =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch NvidiaPlanHostBufferValue identity gpu host extent memory . extent)))
def phBufferIsVideo =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(eliminate
NvidiaPlanHostMemory
(lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat)
memory
(branch NvidiaPlanHostSystemMemory . 0)
(branch NvidiaPlanHostVideoMemory . 1)
(branch NvidiaPlanHostPagedSystemMemory . 0)
(branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
def phBufferIsPaged =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(eliminate
NvidiaPlanHostMemory
(lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat)
memory
(branch NvidiaPlanHostSystemMemory . 0)
(branch NvidiaPlanHostVideoMemory . 0)
(branch NvidiaPlanHostPagedSystemMemory . 1)
(branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
def phBufferIsGPUCached =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
buffer
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(eliminate
NvidiaPlanHostMemory
(lambda unrestricted current : (family NvidiaPlanHostMemory) . Nat)
memory
(branch NvidiaPlanHostSystemMemory . 0)
(branch NvidiaPlanHostVideoMemory . 0)
(branch NvidiaPlanHostPagedSystemMemory . 0)
(branch NvidiaPlanHostGPUCachedSystemMemory . 1)))))
def phABI =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted which : Nat .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . Nat)
abi
(branch
NvidiaPlanHostABIValue
drivers
channel
compute
usermode
engine
userdMemory
channelFlags
directDMAFlags
.
(naturalSelect
(naturalEqual which 4)
channel
(naturalSelect
(naturalEqual which 5)
compute
(naturalSelect
(naturalEqual which 6)
usermode
(naturalSelect (naturalEqual which 7) engine channelFlags))))))))
-- the driver branches the ABI admits
def phDrivers =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . (family NvidiaDriverInterfaces))
abi
(branch NvidiaPlanHostABIValue drivers channel compute usermode engine userdMemory channelFlags directDMAFlags .
drivers)))
-- ---- the driver's branch ----
-- NV_ESC_CHECK_VERSION_STR (0xD2, 72 bytes: cmd, reply, 64 version bytes)
-- with cmd '2', query: the driver writes its own version string. It must
-- begin with the prefix ("580.") of a branch the host's ABI admits, or the
-- host stops, naming `driver-branch`, before any card call -- a 580-ABI host
-- on a 575 driver used to run until its DMA map failed (exit 120 at
-- `dma-map`), and on a 570 driver it faulted. Measured on the RTX 3090,
-- 2026-09-24: driver 580.178.04 answers `580.178.04`, reply 1. A driver
-- that does not answer leaves the bytes zero and is refused the same way.
def phCheckVersionIoctl : Nat =
0xC04846D2
def phVersion : Nat =
1024
-- NV_ESC_CHECK_VERSION_STR owns two u32 fields followed by the fixed version
-- string. Retain the complete query response, including its NUL padding.
def phDriverVersionAt : Nat =
(naturalAdd phVersion (naturalMultiply 2 4))
def phDriverVersionBytes : Nat =
64
-- The selected branch: its 1-based position in the ABI's driver list, for
-- phDriverChoice. Written only when the ABI admits several branches. It
-- follows the version query's 72 bytes, below the error notifier's block.
def phDriverSelection : Nat =
(naturalAdd phVersion 72)
def phDriverSelectionFits :
(equal Nat (naturalLessOrEqual (naturalAdd phDriverSelection 8) phErr) 1) =
(refl Nat 1)
-- The version's first bytes, as many as the branch's prefix has, in an
-- otherwise zero word: what the branch's prefix word is compared with.
def phDriverPrefixLoad =
(lambda unrestricted driver : (family NvidiaDriverInterface) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
phScratch
(phZeros 8)
(phCopyStateToState
phScratch
phDriverVersionAt
(bytes-length (nvidiaDriverInterfacePrefix driver))
tail))))
-- a branch at position `index`: its prefix compared, its position written
-- on a match
def phDriverMatch =
(lambda unrestricted driver : (family NvidiaDriverInterface) .
(lambda unrestricted index : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phDriverPrefixLoad driver
(nativeWhenEqual
(phLoad phScratch)
(phImm (nvidiaDriverInterfacePrefixWord driver))
b"driver-branch-match"
(phNext
(constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState phDriverSelection) (phImm index))
(constructor NativePhysicalCommands NativePhysicalCommandsEnd))
tail)))))
def phDriverMatches =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(eliminate
NvidiaDriverInterfaces
(lambda unrestricted current : (family NvidiaDriverInterfaces) .
(pi unrestricted index : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))
drivers
(branch NvidiaDriverInterfacesLast final .
(lambda unrestricted index : Nat . (phDriverMatch final index)))
(branch NvidiaDriverInterfacesNext head rest induction .
(lambda unrestricted index : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phDriverMatch head index (induction (succ index) tail)))))))
-- Run-time selection (NvidiaDriverInterface): the version
-- text in phVersion selects the first admitted branch whose prefix it
-- begins with (nvidiaDriverInterfaceSelection is the statement; the
-- driver-selection gate runs these commands against it). One branch: its
-- prefix is asserted, as it always was. Several: the selection word starts
-- at 0, each branch whose prefix matches writes its position (admission
-- forbids two branches with one major, so at most one does), and a word
-- still 0 refuses. Every refusal names `driver-branch`; nothing after it
-- runs, so no layout is ever tried on a driver it was not built for.
def phSelectDriverInterface =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nat-eliminate
(lambda unrestricted several : Nat . (family NativePhysicalCommands))
(let unrestricted only = (nvidiaDriverInterfacesFirst drivers) in
(phDriverPrefixLoad only
(nativeLaunchRecipeAssertEqual
(phLoad phScratch)
(phImm (nvidiaDriverInterfacePrefixWord only))
b"driver-branch"
tail)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (family NativePhysicalCommands) .
(phNext
(constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState phDriverSelection) (phImm 0))
(phDriverMatches drivers 1
(nativeWhenEqual
(phLoad phDriverSelection)
(phImm 0)
b"driver-branch"
(nativeLaunchRecipeAssertEqual
(phImm 0)
(phImm 1)
b"driver-branch"
(constructor NativePhysicalCommands NativePhysicalCommandsEnd))
tail)))))
(naturalLess 1 (nvidiaDriverInterfacesCount drivers)))))
-- `body` behind a forward skip unless the selection word is `index`
-- (Runtime.NativeBranch.nativeWhenEqual, which leaves a caller's
-- loop-affine coordinates alone)
def phDriverGuard =
(lambda unrestricted index : Nat .
(lambda unrestricted body :
(pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nativeWhenEqual
(phLoad phDriverSelection)
(phImm index)
b"driver-branch-choice"
(body (constructor NativePhysicalCommands NativePhysicalCommandsEnd))
tail))))
def phDriverGuards =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(lambda unrestricted commands :
(pi unrestricted driver : (family NvidiaDriverInterface) .
(pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
(eliminate
NvidiaDriverInterfaces
(lambda unrestricted current : (family NvidiaDriverInterfaces) .
(pi unrestricted index : Nat . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))
drivers
(branch NvidiaDriverInterfacesLast final .
(lambda unrestricted index : Nat . (phDriverGuard index (commands final))))
(branch NvidiaDriverInterfacesNext head rest induction .
(lambda unrestricted index : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phDriverGuard index (commands head) (induction (succ index) tail))))))))
-- `commands` of the branch the running driver was selected as. One
-- admitted branch: its commands, unguarded. Several: each branch's commands
-- behind its guard. Every admitted branch can run on some admitted host,
-- so none of these bodies is code the pairing does not run; a branch the
-- ABI does not admit has no body at all.
def phDriverChoice =
(lambda unrestricted drivers : (family NvidiaDriverInterfaces) .
(lambda unrestricted commands :
(pi unrestricted driver : (family NvidiaDriverInterface) .
(pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nat-eliminate
(lambda unrestricted several : Nat . (family NativePhysicalCommands))
(commands (nvidiaDriverInterfacesFirst drivers) tail)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (family NativePhysicalCommands) .
(phDriverGuards drivers commands 1 tail)))
(naturalLess 1 (nvidiaDriverInterfacesCount drivers))))))
def phUSERDRequiresVideo =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . Nat)
abi
(branch
NvidiaPlanHostABIValue
drivers
channel
compute
usermode
engine
userdMemory
channelFlags
directDMAFlags
.
(eliminate
NvidiaPlanHostMemory
(lambda unrestricted memory : (family NvidiaPlanHostMemory) . Nat)
userdMemory
(branch NvidiaPlanHostSystemMemory . 0)
(branch NvidiaPlanHostVideoMemory . 1)
(branch NvidiaPlanHostPagedSystemMemory . 0)
(branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
def phIsUVM =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM entries . 0)
(branch NvidiaPlanHostUVM base extent . 1)))
-- the UVM lifecycle's GPFIFO: 0x8000 entries of 8 bytes in the video GPFIFO
-- buffer, USERD the page after them
def nvidiaPlanHostUVMGPFIFOEntries : Nat =
0x8000
def nvidiaPlanHostUVMGPFIFOBytes : Nat =
(naturalMultiply nvidiaPlanHostUVMGPFIFOEntries 8)
-- the direct-RM ring the probes and checked paths allocate
def nvidiaPlanHostDirectGPFIFOEntries : Nat =
0x400
-- the channel's GPFIFO entries: the UVM lifecycle's 0x8000, or the
-- direct-RM lifecycle's own
def phRingEntries =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM entries . entries)
(branch NvidiaPlanHostUVM base extent . nvidiaPlanHostUVMGPFIFOEntries)))
-- a buffer extent for a table: the table's bytes rounded up to a unit
def nvidiaPlanHostRoundUp =
(lambda unrestricted value : Nat .
(lambda unrestricted unit : Nat .
(naturalMultiply
(naturalDivideUnchecked (naturalAdd value (naturalSaturatingSubtract unit 1)) unit)
unit)))
-- Where the host may write: the host-mapped buffers of a layout (host 0 =
-- not mapped), the error notifier's page among them. A range is admitted
-- when mapped buffers cover it end to end -- adjacent mappings may carry
-- one table across their seam (Coppelius's QMD primary and overflow).
def nvidiaPlanHostErrorPageBytes : Nat =
0x1000
def phMapped =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted rest : (family NvidiaPlanHostBuffers) .
(constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext buffer rest)))
def phLayoutMappings =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(phMapped
gpfifo
(phMapped
push
(phMapped
sem
(phMapped
program
(phMapped
qmd
(phMapped
userd
(phMapped
(constructor
NvidiaPlanHostBuffer
NvidiaPlanHostBufferValue
b"error-notifier"
0
errorHost
nvidiaPlanHostErrorPageBytes
(constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory))
data))))))))))
def phMappingCount =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat)
buffers
(branch NvidiaPlanHostBuffersEnd . 0)
(branch NvidiaPlanHostBuffersNext head rest induction . (succ induction))))
-- the end of the first host-mapped buffer holding the byte at `host`, 0 when none does
def phMappingEndAt =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted host : Nat .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat)
buffers
(branch NvidiaPlanHostBuffersEnd . 0)
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(naturalSelect
(naturalAnd
(naturalNonzero (phBufferHost head))
(naturalAnd
(naturalLessOrEqual (phBufferHost head) host)
(naturalLess host (naturalAdd (phBufferHost head) (phBufferExtent head)))))
(naturalAdd (phBufferHost head) (phBufferExtent head))
induction)))))
-- 1 when the buffers cover [host, host + extent): step from mapping to
-- mapping, at most once per mapping (the fuel)
def phCovers =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted fuel : Nat .
(nat-eliminate
(lambda unrestricted current : Nat .
(pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)))
(lambda unrestricted host : Nat .
(lambda unrestricted extent : Nat . (naturalEqual extent 0)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (pi unrestricted host : Nat . (pi unrestricted extent : Nat . Nat)) .
(lambda unrestricted host : Nat .
(lambda unrestricted extent : Nat .
(let unrestricted end =
(phMappingEndAt buffers host)
in
(naturalSelect
(naturalEqual extent 0)
1
(naturalSelect
(naturalEqual end 0)
0
(induction end (naturalSaturatingSubtract (naturalAdd host extent) end)))))))))
fuel)))
def nvidiaPlanHostContains =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted host : Nat .
(lambda unrestricted extent : Nat .
(let unrestricted mappings =
(phLayoutMappings layout)
in
(phCovers mappings (phMappingCount mappings) host extent)))))
-- a GPU-cached buffer is CPU-uncached (MAP_NOT_REQUIRED): no host address
def phGPUCachedUnmapped =
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat)
buffers
(branch NvidiaPlanHostBuffersEnd . 1)
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(naturalAnd
induction
(naturalSelect (phBufferIsGPUCached head) (naturalIsZero (phBufferHost head)) 1)))))
-- Admission, 1 when the host will be derived: the GPFIFO buffer holds the
-- lifecycle's ring; under direct-RM the USERD
-- buffer has the target ABI's location (Ampere requires video memory;
-- the integrated GB10 profile requires system memory). Under
-- UVM the USERD entry is the alias of the GPFIFO's last page and is not
-- allocated, so there is nothing to admit. A pairing gates its artifact
-- on this and the checker decides it.
def nvidiaPlanHostLayoutAdmitted =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat)
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(naturalAnd
(phGPUCachedUnmapped (phLayoutMappings layout))
-- every driver branch the host may select is a well-formed,
-- evidenced layout, and no branch appears twice
(naturalAnd
(nvidiaDriverInterfacesAdmitted (phDrivers abi))
-- the GPFIFO buffer holds the channel's ring
(naturalAnd
(naturalLessOrEqual (naturalMultiply 8 (phRingEntries lifecycle)) (phBufferExtent gpfifo))
(naturalSelect
(phIsUVM lifecycle)
1
(naturalEqual (phBufferIsVideo userd) (phUSERDRequiresVideo abi)))))))))
-- ---- the layout's placement certificate ----
-- Every buffer of a layout is a resident of two arenas: the card's virtual
-- address space (49 bits on Ampere) at its GPU address, and the process's
-- (47 bits of user space) at its host address when it is mapped there. In
-- each, Runtime.ArenaCertificate decides every resident page-aligned,
-- non-empty, inside, and disjoint from every other -- PlanHost's own fixed
-- mappings (the parameter page, the doorbell) and, under UVM, the channel's
-- range among them. The one sanctioned alias, the UVM USERD entry (the
-- GPFIFO buffer's last page, never allocated), is not a resident: it must
-- lie inside the GPFIFO buffer in both spaces.
def nvidiaPlanHostPageBytes : Nat =
0x1000
def phGPUSpaceBytes : Nat =
0x2_0000_0000_0000
def phHostSpaceBytes : Nat =
0x8000_0000_0000
def phResident =
(lambda unrestricted identity : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted rest : (family ArenaResidents) .
(constructor
ArenaResidents
ArenaResidentsNext
(constructor
ArenaResident
ArenaResidentValue
identity
offset
extent
nvidiaPlanHostPageBytes)
rest)))))
-- a buffer at its GPU address
def phGPUResident =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted rest : (family ArenaResidents) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents))
buffer
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(phResident identity gpu extent rest)))))
-- a buffer at its host address, when it is mapped (host 0 = not mapped)
def phHostResident =
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted rest : (family ArenaResidents) .
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . (family ArenaResidents))
buffer
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(nat-eliminate
(lambda unrestricted current : Nat . (family ArenaResidents))
rest
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family ArenaResidents) .
(phResident identity host extent rest)))
(naturalNonzero host))))))
def phEachResident =
(lambda unrestricted place : (pi unrestricted buffer : (family NvidiaPlanHostBuffer) . (pi unrestricted rest : (family ArenaResidents) . (family ArenaResidents))) .
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted rest : (family ArenaResidents) .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) . (family ArenaResidents))
buffers
(branch NvidiaPlanHostBuffersEnd . rest)
(branch NvidiaPlanHostBuffersNext head tail induction . (place head induction))))))
-- the layout's buffers, the USERD entry only when it is allocated (direct-RM)
def phAllocatedBuffers =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostBuffers))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(phMapped
gpfifo
(phMapped
push
(phMapped
sem
(phMapped
program
(phMapped
qmd
(nat-eliminate
(lambda unrestricted current : Nat . (family NvidiaPlanHostBuffers))
(phMapped userd data)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family NvidiaPlanHostBuffers) . data))
(phIsUVM lifecycle))))))))))
-- Count allocations by their actual memory kind. GPU-cached system memory
-- is host memory, and the UVM USERD alias is not a second allocation.
def nvidiaPlanHostVideoAllocationBytes =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) . Nat)
(phAllocatedBuffers layout)
(branch NvidiaPlanHostBuffersEnd . 0)
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(naturalAdd (naturalMultiply (phBufferIsVideo head) (phBufferExtent head)) induction))))
def phGPUResidents =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(phEachResident
phGPUResident
(phAllocatedBuffers layout)
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) .
(family ArenaResidents))
lifecycle
(branch NvidiaPlanHostDirectRM entries . (constructor ArenaResidents ArenaResidentsEnd))
(branch
NvidiaPlanHostUVM
base
extent
.
(phResident
b"uvm-channel-range"
phUVMChannelRangeBase
phUVMChannelRangeExtent
(constructor ArenaResidents ArenaResidentsEnd))))))))
-- `extras`: the mappings a host adds of its own (the request host's recipe
-- staging area)
def phHostResidentsS =
(lambda unrestricted session : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted extras : (family ArenaResidents) .
(phEachResident
phHostResident
(phAllocatedBuffers layout)
(phResident
b"parameters"
phParams
nvidiaPlanHostParameterMappingBytes
(phResident
b"doorbell"
(phDoorHostS session)
0x10000
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family ArenaResidents))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(nat-eliminate
(lambda unrestricted current : Nat . (family ArenaResidents))
extras
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family ArenaResidents) .
(phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes extras)))
(naturalNonzero errorHost))))))))))
def phHostResidents =
(phHostResidentsS 0)
-- [inner, inner + innerExtent) inside [outer, outer + outerExtent)
def phInside =
(lambda unrestricted inner : Nat .
(lambda unrestricted innerExtent : Nat .
(lambda unrestricted outer : Nat .
(lambda unrestricted outerExtent : Nat .
(naturalAnd
(naturalLessOrEqual outer inner)
(naturalLessOrEqual (naturalAdd inner innerExtent) (naturalAdd outer outerExtent)))))))
-- under UVM, the USERD entry inside the GPFIFO buffer in both spaces
def phUSERDAliasInside =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat)
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(naturalSelect
(phIsUVM lifecycle)
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
userd
(branch
NvidiaPlanHostBufferValue
aliasIdentity
aliasGPU
aliasHost
aliasExtent
aliasMemory
.
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
gpfifo
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(naturalAnd
(phInside aliasGPU aliasExtent gpu extent)
(phInside aliasHost aliasExtent host extent))))))
1))))
-- 1 when the layout's placement is certified in both spaces
def nvidiaPlanHostLayoutCertifiedS =
(lambda unrestricted session : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted extras : (family ArenaResidents) .
(naturalAnd
(arenaCertificate phGPUSpaceBytes (phGPUResidents layout))
(naturalAnd
(arenaCertificate phHostSpaceBytes (phHostResidentsS session layout extras))
(phUSERDAliasInside layout))))))
def nvidiaPlanHostLayoutCertified =
(nvidiaPlanHostLayoutCertifiedS 0)
-- Every upload lands inside a host-mapped buffer of the layout: bytes, or a
-- file's declared extent. The subagent's RTX 3070 sweep (2026-09-23) found
-- program tables up to 7936 bytes built into a 4096-byte program buffer and
-- copied past it at run time -- the kernel never ran; now the build refuses.
def nvidiaPlanHostFillsAdmitted =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(eliminate
NvidiaPlanHostFills
(lambda unrestricted current : (family NvidiaPlanHostFills) . Nat)
fills
(branch NvidiaPlanHostFillsEnd . 1)
(branch
NvidiaPlanHostFillBytes
host
payload
rest
induction
.
(naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction))
(branch
NvidiaPlanHostFillFile
host
path
extent
rest
induction
.
(naturalAnd (nvidiaPlanHostContains layout host extent) induction)))))
-- what a plan-derived host needs admitted before it is built
def nvidiaPlanHostAdmittedS =
(lambda unrestricted session : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(naturalAnd
(nvidiaPlanHostLayoutAdmitted layout)
(naturalAnd
(nvidiaPlanHostLayoutCertifiedS session layout (constructor ArenaResidents ArenaResidentsEnd))
(nvidiaPlanHostFillsAdmitted layout fills))))))
def nvidiaPlanHostAdmitted =
(nvidiaPlanHostAdmittedS 0)
-- system memory: host-cached, contiguous or noncontiguous as declared. video memory: the local-user
-- object, write-combined, contiguous, page-aligned.
-- system memory's attributes: PCI, cached, and contiguous (0x32000000) or,
-- paged, non-contiguous (0x2A000000)
def phGPUCachedPageBytes : Nat =
0x10000
-- NV_MEMORY_ALLOCATION_PARAMS for a buffer: owner, flags (8), attr (24),
-- attr2 (28), format (32), size (64), alignment (72), limit (88)
def phGPUCachedMemoryParams =
(lambda unrestricted extent : Nat .
(phSet64
(phSet64
(phSet64
(phSet32
(phSet32
(phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 8 0x0000C001) 24 0x0B000000)
28
0x00000005)
32
0x00000006)
64
extent)
72
phGPUCachedPageBytes)
88
(naturalSaturatingSubtract extent 1)))
def phMemoryParams =
(lambda unrestricted video : Nat .
(lambda unrestricted paged : Nat .
(lambda unrestricted cached : Nat .
(lambda unrestricted inside : Nat .
(lambda unrestricted extent : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(phSet64
(phSet32
(phSet32 (phZeros 128) 0 0x636c6161)
24
(naturalSelect paged 0x2A000000 0x32000000))
64
extent)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes . (phGPUCachedMemoryParams extent)))
cached)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes .
(phSet64
(phSet64
(phSet32
(phSet32 (phSet32 (phZeros 128) 0 0x48454C49) 8 0x00008000)
24
(naturalSelect inside 0x58000000 0x50000000))
64
extent)
72
0x1000)))
video))))))
def phMemoryClass =
(lambda unrestricted video : Nat . (naturalSelect video 0x40 0x3E))
-- the host mapping of one buffer through a fresh control descriptor, or for
-- video memory through a fresh card descriptor
-- phCardPath occupies the unused tail of the UVM control block's page of
-- host state. Its size derives from the longest admitted device path.
def phCardPath : Nat =
(naturalAdd phUVMControl 32)
def phCardPathBytes : Nat =
(bytes-length
(nvidiaDeviceBindingPath
(constructor NvidiaDeviceBinding NvidiaDeviceBindingValue nvidiaCardMinorMaximum b"")))
def phCardPathFits :
(equal Nat (naturalLessOrEqual (naturalAdd phCardPath phCardPathBytes) (phBufferStatus 0)) 1) =
(refl Nat 1)
def phOpenMappingPath =
(lambda unrestricted path : (family NativePhysicalOperand) .
(lambda unrestricted payload : Bytes .
(lambda unrestricted card : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) path (phImm phOpenFlags))
payload
(phStore phSlotMap)
(nativeDescriptorRequire
(phSlot phSlotMap)
phSlotTransfer
b"mapping-open"
(phWhen
card
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phCopy
phWait
(phSet32 (phZeros 8) 0 phStatusSentinel)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotMap) (phImm phWaitOpen) (phState phWait))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm 0)
b"mapping-wait-open"
(phAssertStateZero32 b"mapping-open-status" phWait rest)))))
(phCall
phSysDup2
(phArgs3 (phSlot phSlotMap) (phImm phFdMap) (phImm 0))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm phFdMap)
b"mapping-descriptor"
tail)))))))))
def phMappingDescriptor =
(lambda unrestricted video : Nat .
(nat-eliminate
(lambda unrestricted value : Nat .
(pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)))
(phOpenMappingPath phPayload b"/dev/nvidiactl\x00" 0)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(phOpenMappingPath (phState phCardPath) b"" 1)))
video))
-- the host mapping of one RM memory object: the NVOS33 map through the
-- fresh descriptor, its status recorded, then mmap at the host address
def phMapMemoryS =
(lambda unrestricted session : Nat .
(lambda unrestricted identity : Bytes .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted block : Nat .
(lambda unrestricted hMemory : Nat .
(lambda unrestricted video : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted host : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted flags =
(naturalSelect video 0x01010000 0x03008000)
in
(phMappingDescriptor
video
(phCall
phSysIoctl
(phArgs3 (phImm phFdMap) (phImm phRegisterFD) (phImm phRegFdP))
b""
phDiscard
(phCopy
block
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32 (phSet32 (phZeros 56) 4 (phHDeviceS session)) 8 hMemory)
24
extent)
40
phStatusSentinel)
44
flags)
48
phFdMap)
(phCopyStateToState
block
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState block))
b""
phDiscard
(phCopyStateToState
statusOffset
(naturalAdd block 40)
4
(phCheckStateZero32
identity
(phTolerate mode)
(naturalAdd block 40)
(phCall
phSysMmap
(phArgs
(phImm host)
(phImm extent)
(phImm 3)
(phImm phMapSharedFixed)
(phImm phFdMap)
(phImm 0))
b""
phDiscard
tail)))))))))))))))))))
def phMapMemory =
(phMapMemoryS 0)
def phHostMapS =
(lambda unrestricted session : Nat .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phMapMemoryS session
b"host-map"
mode
(naturalAdd (phBufferState index) 128)
(phHMemoryS session index)
(phBufferIsVideo buffer)
(phBufferExtent buffer)
(phBufferHost buffer)
(naturalAdd (phBufferStatus index) 12)
tail))))))
def phHostMap =
(phHostMapS 0)
def phDirectDMAFlags =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . Nat)
abi
(branch
NvidiaPlanHostABIValue
drivers
channel
compute
usermode
engine
userdMemory
channelFlags
directDMAFlags
.
directDMAFlags)))
-- NV_ESC_RM_MAP_MEMORY_DMA (NVOS46) of the buffer `index`: map the memory
-- object into `handle` (the virtual reservation, or UVM's DMA selector) at
-- `gpu`, with `flags`. The structure's size, the DMA offset's and the
-- status's positions, and the ioctl number are the driver branch's
-- (phDriverChoice): each admitted branch's call is emitted, and the one the
-- running driver was selected as runs. The status lands in the buffer's
-- status record (+8) and, under Strict, must be zero.
def phMapDMAS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted identity : Bytes .
(lambda unrestricted tolerate : Nat .
(lambda unrestricted index : Nat .
(lambda unrestricted handle : Nat .
(lambda unrestricted flags : Nat .
(lambda unrestricted gpu : Nat .
(lambda unrestricted extent : Nat .
(let unrestricted st = (naturalAdd (phBufferState index) 64) in
(phDriverChoice
(phDrivers abi)
(lambda unrestricted driver : (family NvidiaDriverInterface) .
(lambda unrestricted after : (family NativePhysicalCommands) .
(let unrestricted status = (naturalAdd st (nvidiaDriverInterfaceNVOS46StatusOf driver)) in
(phCopy
st
(phSet32
(phSet64
(phSet64
(phSet32
(phSet32
(phSet32
(phSet32 (phZeros (nvidiaDriverInterfaceNVOS46SizeOf driver)) 4 (phHDeviceS session))
8
handle)
12
(phHMemoryS session index))
32
flags)
24
extent)
(nvidiaDriverInterfaceNVOS46DMAOffsetOf driver)
gpu)
(nvidiaDriverInterfaceNVOS46StatusOf driver)
phStatusSentinel)
(phCopyStateToState
st
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3
(phSlot phSlotControl)
(phImm (nvidiaDriverInterfaceMapDMAIoctlOf driver))
(phState st))
b""
phDiscard
(phCopyStateToState
(naturalAdd (phBufferStatus index) 8)
status
4
(phCheckStateZero32 identity tolerate status after)))))))))))))))))))
def phMapDMA =
(phMapDMAS 0)
-- direct-RM: a fixed virtual reservation and the DMA map to it
def phDirectRangeS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted st =
(phBufferState index)
in
(let unrestricted gpu =
(phBufferGPU buffer)
in
(let unrestricted extent =
(phBufferExtent buffer)
in
(phFill
(phVirtP index)
(phSet32
(phSet64
(phSet64 (phZeros 24) 0 gpu)
8
(naturalSaturatingSubtract (naturalAdd gpu extent) 1))
16
(phHVASpaceS session))
(phAlloc
b"alloc:virtual"
(phTolerate mode)
(naturalAdd st 32)
(phHDeviceS session)
0x70
(phVirtP index)
24
(phHVirtualS session index)
(naturalAdd (phBufferStatus index) 4)
(phMapDMAS session
abi
b"dma-map"
(phTolerate mode)
index
(phHVirtualS session index)
(phDirectDMAFlags abi)
gpu
extent
tail))))))))))))
def phDirectRange =
(phDirectRangeS 0)
-- NVOS46 flags of the UVM path's DMA map: DMA_OFFSET_FIXED, CACHE_SNOOP,
-- and 4 KiB pages; a GPU-cached buffer takes the allocation's own (64 KiB)
-- page size instead
def phUVMDMAFlags : Nat =
0x8110
def phUVMDMAFlagsDefaultPages : Nat =
0x8010
-- UVM: an external range at the plan's address, the DMA map through the
-- device DMA selector, and the mapping registered with UVM
def phUVMRangeS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted inside : Nat .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted st =
(phBufferState index)
in
(let unrestricted gpu =
(phBufferGPU buffer)
in
(let unrestricted extent =
(phBufferExtent buffer)
in
(let unrestricted tolerate =
(phTolerate mode)
in
(phWhen
(naturalIsZero inside)
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phFill
phUVMCreateRangeP
(phSet32
(phSet64 (phSet64 (phZeros 24) 0 gpu) 8 extent)
16
phStatusSentinel)
(phUVMCall
b"uvm-buffer-range"
(naturalAdd 8 (naturalMultiply 2 index))
tolerate
phFdUVM
phUVMCreateExternalRange
phUVMCreateRangeP
16
rest)))
(phMapDMAS session
abi
b"dma-map-uvm"
tolerate
index
(phHDMAS session)
(naturalSelect
(phBufferIsGPUCached buffer)
phUVMDMAFlagsDefaultPages
phUVMDMAFlags)
gpu
extent
(phFill
phUVMMapAllocationP
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32
(phSet64 (phSet64 (phZeros 9264) 0 gpu) 8 extent)
40
1)
9240
1)
9248
phFdControl)
9256
(phHMemoryS session index))
9260
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
(naturalAdd phUVMMapAllocationP 24)
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMMapAllocationP 9252)
4
(phUVMCall
b"uvm-buffer-map"
(naturalAdd 9 (naturalMultiply 2 index))
tolerate
phFdUVM
phUVMMapExternalAllocation
phUVMMapAllocationP
9260
tail)))))))))))))))))
def phUVMRange =
(phUVMRangeS 0)
-- One buffer: allocate, place, map.
def phBufferS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted video =
(phBufferIsVideo buffer)
in
(let unrestricted uvm =
(phIsUVM lifecycle)
in
(let unrestricted inside =
(phInsideRange lifecycle (phBufferGPU buffer) (phBufferExtent buffer))
in
(phFill
(phMemP index)
(phMemoryParams
video
(phBufferIsPaged buffer)
(phBufferIsGPUCached buffer)
inside
(phBufferExtent buffer))
(phAlloc
(bytes-append b"alloc:" (phBufferIdentity buffer))
(phTolerate mode)
(phBufferState index)
(phHDeviceS session)
(phMemoryClass video)
(phMemP index)
128
(phHMemoryS session index)
(phBufferStatus index)
(phWhen
(naturalIsZero uvm)
(phDirectRangeS session abi mode index buffer)
(phWhen
uvm
(phUVMRangeS session abi mode inside index buffer)
(phWhen
(naturalNonzero (phBufferHost buffer))
(phHostMapS session mode index buffer)
tail)))))))))))))))
def phBuffer =
(phBufferS 0)
def phDataBuffersS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted first : Nat .
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) .
(pi unrestricted index : Nat . (family NativePhysicalCommands)))
buffers
(branch NvidiaPlanHostBuffersEnd . (lambda unrestricted index : Nat . tail))
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(lambda unrestricted index : Nat .
(phBufferS session abi mode lifecycle index head (induction (succ index))))))
first))))))))
def phDataBuffers =
(phDataBuffersS 0)
-- ---- device discovery ----
-- Binding is a deployment input. All checks here are strict even for a
-- diagnostic channel probe: a probe must never diagnose a different GPU.
def phOpenSelectedCardS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nativeLaunchRecipeAssertEqual
(phImm (nvidiaDeviceBindingAdmitted device))
(phImm 1)
b"device-binding"
(phCopy
phCardPath
(nvidiaDeviceBindingPath device)
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) (phState phCardPath) (phImm phOpenFlags))
b""
(phStore phSlotGPU)
(nativeDescriptorRequire
(phSlot phSlotGPU)
phSlotTransfer
b"card-open"
(phCopy
phWait
(phSet32 (phZeros 8) 0 phStatusSentinel)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotGPU) (phImm phWaitOpen) (phState phWait))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm 0)
b"card-wait-open"
(phAssertStateZero32
b"card-open-status"
phWait
(phCall
phSysDup2
(phArgs3 (phSlot phSlotGPU) (phImm (phFdCardS session)) (phImm 0))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm (phFdCardS session))
b"card-descriptor"
tail)))))))))))))
def phOpenSelectedCard =
(phOpenSelectedCardS 0)
-- The inventory follows the largest live UVM parameter block and fits the
-- owner's mapped parameter arena. It is consumed before any buffer mapping.
def phCardInfoP : Nat =
(nvidiaPlanHostRoundUp (naturalAdd phUVMMapAllocationP 9264) 64)
def phCardInfoFits :
(equal
Nat
(naturalLessOrEqual
(naturalAdd phCardInfoP nvidiaCardInfoBytes)
(naturalAdd phParams nvidiaPlanHostParameterMappingBytes))
1) =
(refl Nat 1)
def phBindSelectedDeviceS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phCardInfoP
(phZeros nvidiaCardInfoBytes)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm nvidiaCardInfoIoctl) (phImm phCardInfoP))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm 0)
b"card-inventory"
(phNext
(constructor
NativePhysicalOperation
NativePhysicalMachineRoutine
nvidiaCardInfoGPUIdCode
(nativeLaunchRecipeArguments
(phState phScratch)
(phImm phCardInfoP)
(phImm nvidiaCardInfoMaximumRows)
(phImm (nvidiaDeviceBindingMinor device)))
(phStore phSlotTransfer))
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm 0)
b"card-inventory-selection"
(phFill
phDevP
(phZeros nvidiaDeviceInfoBytes)
(phCopyStateToMapped
phScratch
phDevP
4
(phControl
b"device-id-info"
0
(phRMStatusSlot 13)
phUVMControl
0
nvidiaDeviceInfoCommand
phDevP
nvidiaDeviceInfoBytes
(phCopyMappedToState
(naturalAdd phDevP nvidiaDeviceInfoInstanceOffset)
phScratch
8
(phFill
phDevP
(phZeros 56)
(phCopyStateToMapped
phScratch
phDevP
4
(phCopyStateToMapped
(naturalAdd phScratch 4)
phSubP
4
(phAlloc
b"device"
0
phDev
0
0x80
phDevP
56
(phHDeviceS session)
(phRMStatusSlot 13)
tail))))))))))))))))
def phBindSelectedDevice =
(phBindSelectedDeviceS 0)
-- Compare one complete mapped word against its admitted expected byte slice.
-- Name and UUID checks share the same transfer and comparison mechanism.
def phCompareMappedWord =
(lambda unrestricted error : Bytes .
(lambda unrestricted address : Nat .
(lambda unrestricted expected : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopyMappedToState
(naturalAdd address offset)
phScratch
8
(phCopy
(naturalAdd phScratch 8)
(phTake 8 (phDrop offset expected))
(nativeLaunchRecipeAssertEqual
(phLoad phScratch)
(phLoad (naturalAdd phScratch 8))
error
tail))))))))
-- NV2080_CTRL_CMD_GPU_GET_NAME_STRING: require the pairing's 64 ASCII bytes.
-- Another card refuses by name, `card-name`, before any buffer is allocated:
-- an artifact never runs on a GPU its pairing did not name.
def phNameWord =
(phCompareMappedWord b"card-name" (naturalAdd phNameP 4))
def phExpectNameS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted expected : Bytes .
(phDriverChoice
(phDrivers abi)
(lambda unrestricted driver : (family NvidiaDriverInterface) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phNameP
(phZeros (nvidiaDriverInterfaceNameParamsSizeOf driver))
(phControl
b"control:phName"
(phTolerate mode)
(phRMStatusSlot 11)
phName
(phHSubdeviceS session)
0x20800110
phNameP
(nvidiaDriverInterfaceNameParamsSizeOf driver)
(phNameWord
expected
0
(phNameWord
expected
8
(phNameWord
expected
16
(phNameWord
expected
24
(phNameWord
expected
32
(phNameWord
expected
40
(phNameWord expected 48 (phNameWord expected 56 tail)))))))))))))))))
def phExpectName =
(phExpectNameS 0)
def phExpectDeviceUUIDS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(phWhen
(naturalNonzero (bytes-length (nvidiaDeviceBindingUUID device)))
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phUVMGidP
(phSet32 (phSet32 (phZeros 268) 4 2) 8 nvidiaDeviceUUIDBytes)
(phControl
b"device-uuid"
0
(phRMStatusSlot 12)
phUVMControl
(phHSubdeviceS session)
0x2080014A
phUVMGidP
268
(phCopy
phScratch
(phZeros 8)
(phCopyMappedToState
(naturalAdd phUVMGidP 8)
phScratch
4
(nativeLaunchRecipeAssertEqual
(phLoad phScratch)
(phImm nvidiaDeviceUUIDBytes)
b"device-uuid-length"
(phCompareMappedWord
b"device-uuid"
(naturalAdd phUVMGidP 12)
(nvidiaDeviceBindingUUID device)
0
(phCompareMappedWord
b"device-uuid"
(naturalAdd phUVMGidP 12)
(nvidiaDeviceBindingUUID device)
8
tail)))))))))))
def phExpectDeviceUUID =
(phExpectDeviceUUIDS 0)
-- ---- the UVM driver ----
def phUVMPrepareS =
(lambda unrestricted session : Nat .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted base : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phUVMGidP
(phSet32 (phSet32 (phZeros 268) 4 2) 8 16)
(phControl
b"control:phUVMControl"
(phTolerate mode)
(phRMStatusSlot 12)
phUVMControl
(phHSubdeviceS session)
0x2080014A
phUVMGidP
268
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags))
b"/dev/nvidia-uvm\x00"
(phStore phSlotMap)
(phCall
phSysDup2
(phArgs3 (phSlot phSlotMap) (phImm phFdUVM) (phImm 0))
b""
(phStore phSlotMap)
(phFill
phUVMInitP
(phSet32 (phZeros 16) 8 phStatusSentinel)
(phUVMCallAfterOpen
(phTolerate mode)
b"uvm-initialize"
1
(phTolerate mode)
phFdUVM
phUVMInitialize
phUVMInitP
8
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags))
b"/dev/nvidia-uvm\x00"
(phStore phSlotMap)
(phCall
phSysDup2
(phArgs3 (phSlot phSlotMap) (phImm phFdUVMMemoryMap) (phImm 0))
b""
(phStore phSlotMap)
(phFill
phUVMMMP
(phSet32 (phSet32 (phZeros 8) 0 phFdUVM) 4 phStatusSentinel)
(phUVMCallAfterOpen
(phTolerate mode)
b"uvm-mm-initialize"
2
1
phFdUVMMemoryMap
phUVMMMInitialize
phUVMMMP
4
(phFill
phUVMRegisterGPUP
(phSet32
(phSet32 (phZeros 40) 24 phStatusSentinel)
36
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterGPUP
16
(phUVMCall
b"uvm-register-gpu"
3
(phTolerate mode)
phFdUVM
phUVMRegisterGPU
phUVMRegisterGPUP
36
(phFill
phUVMRegisterVASpaceP
(phSet32
(phSet32
(phSet32 (phZeros 32) 16 phFdControl)
24
(phHVASpaceS session))
28
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterVASpaceP
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMRegisterVASpaceP 20)
4
(phUVMCall
b"uvm-register-vaspace"
4
(phTolerate mode)
phFdUVM
phUVMRegisterGPUVASpace
phUVMRegisterVASpaceP
28
(phWhen
(naturalNonzero extent)
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phFill
phUVMCreateRangeP
(phSet32
(phSet64 (phSet64 (phZeros 24) 0 base) 8 extent)
16
phStatusSentinel)
(phUVMCall
b"uvm-external-range"
6
(phTolerate mode)
phFdUVM
phUVMCreateExternalRange
phUVMCreateRangeP
16
rest)))
tail)))))))))))))))))))))))
def phUVMPrepare =
(phUVMPrepareS 0)
def phUVMRegisterChannelCommandsS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phUVMRegisterChannelP
(phSet32
(phSet64
(phSet64
(phSet32 (phSet32 (phZeros 56) 16 phFdControl) 24 (phHClassS session (phABI abi 4)))
32
phUVMChannelRangeBase)
40
phUVMChannelRangeExtent)
48
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterChannelP
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMRegisterChannelP 20)
4
(phUVMCall
b"uvm-register-channel"
5
(phTolerate mode)
phFdUVM
phUVMRegisterChannel
phUVMRegisterChannelP
48
tail))))))))
def phUVMRegisterChannelCommands =
(phUVMRegisterChannelCommandsS 0)
-- ---- publishing a submission ----
-- gpPut into USERD, SFENCE, the work-submit token into the doorbell: the
-- training runtime's publication routine (x86: mov [rdi], esi; sfence;
-- mov [rdx], ecx), run on this thread, so the doorbell cannot reach the card
-- ahead of gpPut through a write-combining buffer. The token is loaded
-- from the parameter page into the scratch word first.
--
-- Measured on an RTX 3090, driver 580.178.04, 2026-09-24. Before, gpPut
-- went through the pipe copy and the doorbell after it, unordered: 7 hangs
-- in 250 warp-sum runs, and in every one the semaphores were untouched (the
-- device never began the pushbuffer), USERD's GP_PUT 1 and GP_GET 0 (the
-- channel never fetched the entry) -- the doorbell had arrived before
-- gpPut. A membarrier between the two (a locked-instruction barrier, which
-- need not drain write-combining buffers) did not help: 11 hangs in 300
-- against 6 unfenced. This routine: 0 hangs in 300 against 13 unfenced,
-- interleaved on the same card.
def phPublishCode : Bytes =
(eliminate
X86NativeAssemblyResult
(lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
nativePhysicalTrainingGeneratePublish32Routine
(branch X86NativeAssemblyEncoded code . code)
(branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
(branch X86NativeAssemblyEncodeOffsetOverflow . b"")
(branch X86NativeAssemblyMissingLabel name . b"")
(branch X86NativeAssemblyDisplacementOutOfRange name . b""))
def phLoadTokenS =
(lambda unrestricted session : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy phScratch (phZeros 8) (phCopyMappedToState (phTokPS session) phScratch 4 tail))))
def phLoadToken =
(phLoadTokenS 0)
def phPublishOperandS =
(lambda unrestricted session : Nat .
(lambda unrestricted userdGPPut : Nat .
(lambda unrestricted gpPut : (family NativePhysicalOperand) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor
NativePhysicalOperation
NativePhysicalMachineRoutine
phPublishCode
(phArgs
(phImm userdGPPut)
gpPut
(phImm (naturalAdd (phDoorHostS session) 0x90))
(phLoad phScratch)
(phImm 0)
(phImm 0))
phDiscard)
tail)))))
def phPublishOperand =
(phPublishOperandS 0)
def phPublishS =
(lambda unrestricted session : Nat .
(lambda unrestricted userdGPPut : Nat .
(lambda unrestricted gpPut : Nat . (phPublishOperandS session userdGPPut (phImm gpPut)))))
def phPublish =
(phPublishS 0)
-- ---- the doorbell ----
def phDoorbellS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysIoctl
(phArgs3 (phImm (phFdCardS session)) (phImm phRegisterFD) (phImm phRegFdP))
b""
phDiscard
(phCopy
phDoorMap
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32 (phSet32 (phZeros 56) 4 (phHSubdeviceS session)) 8 (phHClassS session (phABI abi 6)))
24
0x10000)
40
phStatusSentinel)
44
0)
48
(phFdCardS session))
(phCopyStateToState
phDoorMap
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState phDoorMap))
b""
phDiscard
(phCopyStateToState
(phRMStatusSlot 18)
(naturalAdd phDoorMap 40)
4
(phCheckStateZero32
b"doorbell-map"
(phTolerate mode)
(naturalAdd phDoorMap 40)
(phCall
phSysMmap
(phArgs
(phImm (phDoorHostS session))
(phImm 0x10000)
(phImm 3)
(phImm phMapSharedFixed)
(phImm (phFdCardS session))
(phImm 0))
b""
phDiscard
tail)))))))))))
def phDoorbell =
(phDoorbellS 0)
def phTokenS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
(phTokPS session)
(phZeros 4)
(phControl
b"control:phTok"
(phTolerate mode)
(phRMStatusSlot 15)
phTok
(phHClassS session (phABI abi 4))
0xc36f0108
(phTokPS session)
4
tail))))))
def phToken =
(phTokenS 0)
-- NVA06C_CTRL_CMD_GPFIFO_SCHEDULE (bEnable = 1) on the channel group; its
-- parameter size is the driver branch's (phDriverChoice)
def phScheduleS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(phDriverChoice
(phDrivers abi)
(lambda unrestricted driver : (family NvidiaDriverInterface) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted size = (nvidiaDriverInterfaceScheduleParamsSizeOf driver) in
(phFill
phSchedP
(phTake size (bytes 1 0 0))
(phControl
b"control:phSched"
(phTolerate mode)
(phRMStatusSlot 14)
phSched
(phHGroupS session)
0xa06c0101
phSchedP
size
tail)))))))))
def phSchedule =
(phScheduleS 0)
def phVASpaceParams =
(lambda unrestricted uvm : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(phZeros 48)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes .
(phSet64 (phSet64 (phSet32 (phZeros 48) 4 0x48) 8 0x1FFFFFB000000) 40 0x1000)))
uvm))
def phUVMLifecycleS =
(lambda unrestricted session : Nat .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) .
(family NativePhysicalCommands))
lifecycle
(branch NvidiaPlanHostDirectRM entries . tail)
(branch NvidiaPlanHostUVM base extent . (phUVMPrepareS session mode base extent tail)))))))
def phUVMLifecycle =
(phUVMLifecycleS 0)
def phDMASelectorS =
(lambda unrestricted session : Nat .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phDMAObjectP
(phSet64 (phZeros 24) 8 0x1FFFFFFFFFFFF)
(phAlloc
b"alloc:phDMAObject"
(phTolerate mode)
phDMAObject
(phHDeviceS session)
0x70
phDMAObjectP
24
(phHDMAS session)
(phRMStatusSlot 2)
tail)))))
def phDMASelector =
(phDMASelectorS 0)
def phDirectActivateS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phBindP
(phW32 1)
(phControl
b"control:phBind"
(phTolerate mode)
(phRMStatusSlot 13)
phBind
(phHClassS session (phABI abi 4))
0xa06f0104
phBindP
4
(phScheduleS session abi mode (phTokenS session abi mode (phDoorbellS session abi mode tail)))))))))
def phDirectActivate =
(phDirectActivateS 0)
def phUVMActivateS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phDoorbellS session
abi
mode
(phFill
phPreemptP
(phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 0 1) 4 (phHGroupS session)) 8 0) 12 2)
(phControl
b"control:phPreempt"
(phTolerate mode)
(phRMStatusSlot 16)
phPreempt
(phHSubdeviceS session)
0x20801210
phPreemptP
32
(phTokenS session abi mode (phUVMRegisterChannelCommandsS session abi mode (phScheduleS session abi mode tail))))))))))
def phUVMActivate =
(phUVMActivateS 0)
-- Where a plan maps its buffers in the process: from the origin, each
-- after the previous at the alignment, in extents of the mapping unit.
-- The host side of the arena certificate decides that they are disjoint
-- and clear of the host's own mappings.
def nvidiaPlanHostMappingOrigin : Nat =
0x6000_0000
def nvidiaPlanHostMappingAlignment : Nat =
0x0200_0000
def nvidiaPlanHostMappingUnit : Nat =
0x10000
-- the USERD page mapped after the GPFIFO entries, and the words of it the
-- host reads: GP_GET and GP_PUT (Accelerator.SM86.USERD's layout, slot 0)
def nvidiaPlanHostUSERDBytes : Nat =
nvidiaPlanHostPageBytes
def nvidiaPlanHostUSERDGPGetOffset : Nat =
0x88
def nvidiaPlanHostUSERDGPPutOffset : Nat =
0x8c
def phChannelParamsS =
(lambda unrestricted session : Nat .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted direct : Nat .
(lambda unrestricted entries : Nat .
(lambda unrestricted gpfifoGPU : Nat .
(phSet32
(phSet64
(phSet32
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32 (phSet32 (phZeros 368) 0 (phHErrorS session)) 4 (phHMemoryS session 0))
8
gpfifoGPU)
16
entries)
20
(naturalSelect direct (phABI abi 10) 0))
24
(phHContextS session))
32
(naturalSelect direct (phHMemoryS session 5) (phHMemoryS session 0)))
64
(naturalSelect direct 0 nvidiaPlanHostUVMGPFIFOBytes))
128
(phABI abi 7)))))))
def phChannelParams =
(phChannelParamsS 0)
def phRootAndDriverBranch =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phAssertStateZero32
b"root"
offset
(phCopy
phVersion
(phSet32 (phZeros 72) 0 0x32)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm phCheckVersionIoctl) (phState phVersion))
b""
phDiscard
(phSelectDriverInterface (phDrivers abi) tail)))))))
-- ---- the prelude: a working compute channel ----
-- The selected card, root client and subdevice are established once. This
-- continuation boundary lets composed native hosts install communication
-- state before channel buffers while retaining the same binding protocol.
def phDeviceSessionS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted expectedName : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted tolerate =
(phTolerate mode)
in
(phOpenSelectedCardS session
device
(phWhen
(naturalIsZero session)
-- the first session opens the control device, allocates the RM
-- client, selects the driver branch and maps the parameter
-- page; every later session uses them (phSessionHandle)
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags))
b"/dev/nvidiactl\x00"
(phStore phSlotControl)
(nativeDescriptorRequire
(phSlot phSlotControl)
phSlotTransfer
b"control-open"
(phCall
phSysDup2
(phArgs3 (phSlot phSlotControl) (phImm phFdControl) (phImm 0))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm phFdControl)
b"control-descriptor"
(phCopy
phRoot
(phSet32 (phZeros 32) 28 phStatusSentinel)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm phRMAlloc) (phState phRoot))
b""
phDiscard
(phCopyStateToState
(phRMStatusSlot 0)
(naturalAdd phRoot 28)
4
(phRootAndDriverBranch
abi
(naturalAdd phRoot 28)
(phCall
phSysMmap
(phArgs
(phImm phParams)
(phImm nvidiaPlanHostParameterMappingBytes)
(phImm 3)
(phImm phMapAnonymousFixed)
(phImm phNoDescriptor)
(phImm 0))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm phParams)
b"device-parameters"
(phFill
phRegFdP
(phW32 phFdControl) rest))))))))))))
(phBindSelectedDeviceS session
device
(phAlloc
b"alloc:phSub"
tolerate
phSub
(phHDeviceS session)
0x2080
phSubP
4
(phHSubdeviceS session)
(phRMStatusSlot 1)
(phExpectDeviceUUIDS session
device
(phWhen
(naturalNonzero (bytes-length expectedName))
(phExpectNameS session abi mode expectedName)
tail)))))))))))))
def phDeviceSession =
(phDeviceSessionS 0)
def phPreludeOnS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family NativePhysicalCommands))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(let unrestricted uvm =
(phIsUVM lifecycle)
in
(let unrestricted direct =
(naturalIsZero uvm)
in
(let unrestricted channelClass =
(phHClassS session (phABI abi 4))
in
(let unrestricted tolerate =
(phTolerate mode)
in
(phDeviceSessionS session
device
mode
abi
expectedName
(phWhen
uvm
(phDMASelectorS session mode)
(phFill
phVASP
(phVASpaceParams uvm)
(phAlloc
b"alloc:phVAS"
tolerate
phVAS
(phHDeviceS session)
0x90f1
phVASP
48
(phHVASpaceS session)
(phRMStatusSlot 3)
(phUVMLifecycleS session
mode
lifecycle
(phBufferS session
abi
mode
lifecycle
0
gpfifo
(phBufferS session
abi
mode
lifecycle
1
push
(phBufferS session
abi
mode
lifecycle
2
sem
(phBufferS session
abi
mode
lifecycle
3
program
(phBufferS session
abi
mode
lifecycle
4
qmd
(phWhen
direct
(phBufferS session abi mode lifecycle 5 userd)
(phDataBuffersS session
abi
mode
lifecycle
6
data
(phFill
phErrP
(phMemoryParams 0 0 0 0 nvidiaPlanHostErrorPageBytes)
(phAlloc
b"alloc:phErr"
tolerate
phErr
(phHDeviceS session)
0x3E
phErrP
128
(phHErrorS session)
(phRMStatusSlot 4)
(phWhen
(naturalNonzero errorHost)
(phMapMemoryS session
b"error-map"
mode
phErrMap
(phHErrorS session)
0
nvidiaPlanHostErrorPageBytes
errorHost
(phRMStatusSlot 7))
(phFill
phGroupP
(phSet32
(phSet32 (phZeros 20) 8 (naturalSelect direct (phHVASpaceS session) 0))
12
1)
(phAlloc
b"alloc:phGroup"
tolerate
phGroup
(phHDeviceS session)
0xa06c
phGroupP
20
(phHGroupS session)
(phRMStatusSlot 5)
(phFill
phCtxP
(phSet32 (phSet32 (phZeros 12) 0 (phHVASpaceS session)) 4 uvm)
(phAlloc
b"alloc:phCtx"
tolerate
phCtx
(phHGroupS session)
0x9067
phCtxP
12
(phHContextS session)
(phRMStatusSlot 6)
(phFill
phChanP
(phChannelParamsS session abi direct (phRingEntries lifecycle) (phBufferGPU gpfifo))
(phAlloc
b"alloc:phChan"
tolerate
phChan
(phHGroupS session)
(phABI abi 4)
phChanP
368
channelClass
(phRMStatusSlot 8)
(phAlloc
b"alloc:phComp"
tolerate
phComp
channelClass
(phABI abi 5)
0
0
(phHClassS session (phABI abi 5))
(phRMStatusSlot 9)
(phAlloc
b"alloc:phUser"
tolerate
phUser
(phHSubdeviceS session)
(phABI abi 6)
0
0
(phHClassS session (phABI abi 6))
(phRMStatusSlot 10)
(phWhen
direct
(phDirectActivateS session abi mode)
(phWhen uvm (phUVMActivateS session abi mode) tail))))))))))))))))))))))))))))))))))))
def phPreludeOn =
(phPreludeOnS 0)
def phPreludeS =
(lambda unrestricted session : Nat .
(phPreludeOnS session nvidiaDeviceZero))
def phPrelude =
(phPreludeS 0)
-- ---- uploads, submission, completion, readback ----
def phFills =
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate
NvidiaPlanHostFills
(lambda unrestricted current : (family NvidiaPlanHostFills) .
(family NativePhysicalCommands))
fills
(branch NvidiaPlanHostFillsEnd . tail)
(branch
NvidiaPlanHostFillBytes
host
payload
rest
induction
.
(phFill host payload induction))
(branch
NvidiaPlanHostFillFile
host
path
extent
rest
induction
.
(phReadFile path host extent induction)))))
def phReads =
(lambda unrestricted reads : (family NvidiaPlanHostReads) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate
NvidiaPlanHostReads
(lambda unrestricted current : (family NvidiaPlanHostReads) .
(family NativePhysicalCommands))
reads
(branch NvidiaPlanHostReadsEnd . tail)
(branch
NvidiaPlanHostReadsNext
host
extent
rest
induction
.
-- A successful fence does not imply a complete output file. Keep
-- write errors and short writes visible before recording read-back;
-- a caller must never interpret a truncated frame as a measurement.
(phCall
phSysWrite
(phArgs3 (phImm 1) (phImm host) (phImm extent))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm extent)
b"readback-write"
induction))))))
def nvidiaPlanHostFenceValue : Nat =
65261
-- The host polls a submission's completion fence, sleeping `interval` ns
-- between reads. A 1 ms sleep rounded every fence wait up to whole wake-ups
-- while the GPU sat idle; Baguette's update makes thousands of submissions.
-- A sleep lasts its interval plus the thread's timer slack (Linux's
-- default, 50 us), so the 20 us sleep this replaced woke ~70 us after a
-- GPT-2 update's four submissions each completed: the GPU idle that long
-- four times an update, and the wake-ups, not the kernels, setting the
-- update's time (a 0.24 ms faster update in the launch profile ran no
-- faster, H100 2026-10-18). The request sets the slack to 1 ns
-- (PlanHostRequest's prTimerSlack) and polls every 2 us: the GPU waits a
-- few microseconds for the next submission, as a CUDA host spinning on its
-- stream would make it; the ~600 s timeout (polls x interval) stays.
def nvidiaPlanHostFenceInterval : Nat =
2000
def nvidiaPlanHostFenceMaximumPolls : Nat =
300000000
def phUSERDHost =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat)
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(phBufferHost userd))))
-- Release everything before exit: freeing the root client tears the whole
-- object hierarchy down synchronously. Left to the driver's asynchronous
-- reclaim at process exit, back-to-back hosts on the RTX 3090 hit
-- NV_ERR_INSUFFICIENT_RESOURCES on the channel allocation about a third of
-- the time, in streaks; v3 of this host, which did not free, did too.
def phRelease =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
phFree
(phSet32 (phZeros 16) 12 phStatusSentinel)
(phCopyStateToState
phFree
(naturalAdd phRoot 8)
4
(phCopyStateToState
(naturalAdd phFree 4)
(naturalAdd phRoot 8)
4
(phCopyStateToState
(naturalAdd phFree 8)
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMFree) (phState phFree))
b""
phDiscard
(phCopyStateToState
(phRMStatusSlot 17)
(naturalAdd phFree 12)
4
(phAssertStateZero32 b"rm-free-root" (naturalAdd phFree 12) tail))))))))
-- The whole host, Strict: `submissions` is gpPut, the number of GPFIFO
-- entries the plan's tables carry; `fenceHost` the host address of the
-- semaphore slot the last submission releases; `statusHost`, when not 0, a
-- mapped address the UVM status record is copied to before the readbacks.
-- ---- native telemetry (docs/observability PRD item 9) ----
-- At each phase boundary the host appends an ALPHATEL record to
-- `alpha-host.alphatel` in its working directory: the body is
-- Runtime.NativeTelemetry's own encoding, made at build time (domain 1,
-- event 1 "reached", the boundary's ordinal as phase and sequence, status
-- 0, its name as payload), with the monotonic nanoseconds left zero; at
-- run time the host reads CLOCK_MONOTONIC and Runtime.NativeTelemetrySeal
-- writes the reading into the body, digests it and writes the record. A
-- record exists only if the host got there, so the last one names how far
-- a failed run came. The write is asserted whole (`telemetry-write`): a
-- host that cannot record says so and stops, rather than running unobserved.
-- Its pages: a fixed anonymous mapping of its own, taken before any device
-- call, so a host with no card still records its beginning.
def phTelemetryPage : Nat =
0x5E000000
def phTelemetryRegionBytes : Nat =
1024
def phTelemetryExtent : Nat =
(naturalMultiply 4 phTelemetryRegionBytes)
def phTelemetryPadded : Nat =
phTelemetryPage
def phTelemetryRecord : Nat =
(naturalAdd phTelemetryPadded phTelemetryRegionBytes)
def phTelemetryClock : Nat =
(naturalAdd phTelemetryRecord phTelemetryRegionBytes)
def phTelemetryWork : Nat =
(naturalAdd phTelemetryClock phTelemetryRegionBytes)
def phSlotTelemetry : Nat =
14
def phSlotTelemetryWritten : Nat =
15
def phTelemetryPath : Bytes =
b"alpha-host.alphatel\x00"
def phSysClockGettime : Nat =
228
def phClockMonotonic : Nat =
1
-- O_WRONLY | O_CREAT | O_APPEND, mode 0600
def phTelemetryOpenFlags : Nat =
1089
def phTelemetryMode : Nat =
384
def phTelemetryDirectoryFlags : Nat =
65536
def phTelemetryIdentity : Bytes =
(bytes-append
phIdentity
(phZeros (naturalSaturatingSubtract nativeTelemetryDigestBytes (bytes-length phIdentity))))
def phTelemetryZero : (family ModelWord64) =
(phWord 0)
-- the body Runtime.NativeTelemetry encodes for boundary `ordinal`, its
-- clock reading zero: no error code, the name as payload
def phTelemetryBody =
(lambda unrestricted ordinal : Nat .
(lambda unrestricted name : Bytes .
(nativeTelemetryRecordBody
(phWord ordinal)
phTelemetryZero
(byte 1)
(byte 1)
(nat-to-byte ordinal)
(byte 0)
(constructor
NativeTelemetryCounters
NativeTelemetryCountersValue
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero)
phTelemetryIdentity
b""
name
phTelemetryZero
(phWord (bytes-length name)))))
-- the body with SHA-256's padding: 0x80, zeros to 56 mod 64, the bit length
-- (big-endian; a body is far below 8 KiB). Reduce the length before
-- subtraction: saturating 567 - length silently broke bodies above 567 bytes.
-- 119 = 55 + 64 keeps subtraction nonnegative for every block remainder.
def phTelemetryPadding =
(lambda unrestricted length : Nat .
(bytes-cons
(byte 128)
(bytes-append
(phZeros
(naturalModuloUnchecked
(naturalSaturatingSubtract 119 (naturalModuloUnchecked length 64))
64))
(bytes-append
(phZeros 6)
(bytes-cons
(nat-to-byte (naturalDivideUnchecked (naturalMultiply 8 length) 256))
(bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalMultiply 8 length) 256)) b""))))))
-- A boundary acknowledges only after the complete frame, its file, and the
-- containing directory have reached the kernel's durability boundary. It is
-- still a legacy v1 phase record; this does not claim batched v3 publication or
-- protect against torn append after a crash. Bind the relative filename to the
-- opened directory rather than reopening a possibly changed working directory.
-- The seal workspace is dead after sealing and safely holds a native stat.
def phTelemetryCheckedCall =
(lambda unrestricted number : Nat .
(lambda unrestricted arguments : (family NativePhysicalArguments) .
(lambda unrestricted error : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
number
arguments
b""
(phStore phSlotTelemetryWritten)
(nativeLaunchRecipeAssertEqual (phSlot phSlotTelemetryWritten) (phImm 0) error tail))))))
def phTelemetryDescriptor =
(lambda unrestricted descriptor : (family NativePhysicalOperand) .
(lambda unrestricted error : Bytes .
(phTelemetryCheckedCall
phSysFstat
(phArgs3 descriptor (phImm phTelemetryWork) (phImm 0))
error)))
def phTelemetryAppend =
(lambda unrestricted length : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phTelemetryDirectoryFlags))
b".\x00"
(phStore phSlotTransfer)
(phTelemetryDescriptor
(phSlot phSlotTransfer)
b"telemetry-directory-open"
(phCall
phSysOpenat
(phArgs
(phSlot phSlotTransfer)
phPayload
(phImm phTelemetryOpenFlags)
(phImm phTelemetryMode)
(phImm 0)
(phImm 0))
phTelemetryPath
(phStore phSlotTelemetry)
(phTelemetryDescriptor
(phSlot phSlotTelemetry)
b"telemetry-open"
(phCall
phSysWrite
(phArgs3 (phSlot phSlotTelemetry) (phImm phTelemetryRecord) (phImm length))
b""
(phStore phSlotTelemetryWritten)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTelemetryWritten)
(phImm length)
b"telemetry-write"
(phTelemetryCheckedCall
phSysFsync
(phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0))
b"telemetry-file-sync"
(phTelemetryCheckedCall
phSysFsync
(phArgs3 (phSlot phSlotTransfer) (phImm 0) (phImm 0))
b"telemetry-directory-sync"
(phTelemetryCheckedCall
phSysClose
(phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0))
b"telemetry-close"
(phTelemetryCheckedCall
phSysClose
(phArgs3 (phSlot phSlotTransfer) (phImm 0) (phImm 0))
b"telemetry-directory-close"
tail))))))))))))
-- Check the fixed mapping before its first fill: MAP_FIXED failure must be a
-- named recording failure, never a fault while touching the intended address.
def phTelemetryOpen =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysMmap
(phArgs
(phImm phTelemetryPage)
(phImm phTelemetryExtent)
(phImm 3)
(phImm phMapAnonymousFixed)
(phImm phNoDescriptor)
(phImm 0))
b""
(phStore phSlotTelemetryWritten)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTelemetryWritten)
(phImm phTelemetryPage)
b"telemetry-map"
(phFill phTelemetryRecord b"ALPHATEL" tail))))
-- Admit both buffers before any copy or seal. Names are build-time data, but
-- their lengths vary with the owning run policy; a long name must never spill
-- the padded body into the record or the record into the clock/workspace.
def phTelemetryBodyFits =
(lambda unrestricted body : Bytes .
(naturalAnd
(naturalLessOrEqual
(naturalAdd (bytes-length body) (bytes-length (phTelemetryPadding (bytes-length body))))
(naturalSaturatingSubtract phTelemetryRecord phTelemetryPadded))
(naturalLessOrEqual
(naturalAdd 72 (bytes-length body))
(naturalSaturatingSubtract phTelemetryClock phTelemetryRecord))))
def phTelemetry =
(lambda unrestricted ordinal : Nat .
(lambda unrestricted name : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted body =
(phTelemetryBody ordinal name)
in
(let unrestricted length =
(bytes-length body)
in
(let unrestricted padded =
(bytes-append body (phTelemetryPadding length))
in
(nativeLaunchRecipeAssertEqual
(phImm (phTelemetryBodyFits body))
(phImm 1)
b"telemetry-frame-extent"
(phFill
phTelemetryPadded
padded
(phCall
phSysClockGettime
(phArgs3 (phImm phClockMonotonic) (phImm phTelemetryClock) (phImm 0))
b""
(phStore phSlotTelemetryWritten)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTelemetryWritten)
(phImm 0)
b"telemetry-clock"
(phNext
(constructor
NativePhysicalOperation
NativePhysicalMachineRoutine
nativeTelemetrySealRoutine
(phArgs
(phImm phTelemetryPadded)
(phImm (naturalDivideUnchecked (bytes-length padded) 64))
(phImm phTelemetryRecord)
(phImm length)
(phImm phTelemetryClock)
(phImm phTelemetryWork))
phDiscard)
(phTelemetryAppend (naturalAdd 72 length) tail))))))))))))
-- Preparation has two ordered phases: envelope validation before any card
-- call, and expansion after the buffers exist. Keeping these continuations
-- here gives recipe-backed probes the same telemetry and submit/wait path
-- as the ordinary host, without copying its RM command stream.
def nvidiaPlanHostPreparedCommandsOnS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted before : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted mapped : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(lambda unrestricted submissions : Nat .
(lambda unrestricted fenceHost : Nat .
(lambda unrestricted statusHost : Nat .
(lambda unrestricted reads : (family NvidiaPlanHostReads) .
(phPipeCreate
(phTelemetryOpen
(phTelemetry
0
b"plan-host:begin"
(before
(phPreludeOnS session
device
(constructor NvidiaPlanHostMode NvidiaPlanHostStrict)
layout
(phTelemetry
1
b"plan-host:channel-ready"
(mapped
(phFills
fills
(phTelemetry
2
b"plan-host:uploaded"
(phLoadTokenS session
(phPublishS session
(naturalAdd
(phUSERDHost layout)
nvidiaPlanHostUSERDGPPutOffset)
submissions
(phTelemetry
3
b"plan-host:submitted"
(phNext
(constructor
NativePhysicalOperation
NativePhysicalFenceWait
(phImm fenceHost)
(phImm nvidiaPlanHostFenceValue)
(phWord nvidiaPlanHostFenceMaximumPolls)
(phWord nvidiaPlanHostFenceInterval))
(phTelemetry
4
b"plan-host:completed"
(phWhen
(naturalNonzero statusHost)
(phCopyStateToMapped
phUVMStatusRecord
statusHost
phUVMStatusRecordExtent)
(phReads
reads
(phTelemetry
5
b"plan-host:read-back"
(phCall
phSysExitGroup
(phArgs3 (phImm 0) (phImm 0) (phImm 0))
b""
phDiscard
(phNext
(constructor
NativePhysicalOperation
NativePhysicalHaltSuccess)
(constructor
NativePhysicalCommands
NativePhysicalCommandsEnd))))))))))))))))))))))))))))))
def nvidiaPlanHostPreparedCommandsOn =
(nvidiaPlanHostPreparedCommandsOnS 0)
def nvidiaPlanHostPreparedCommandsS =
(lambda unrestricted session : Nat .
(nvidiaPlanHostPreparedCommandsOnS session nvidiaDeviceZero))
def nvidiaPlanHostPreparedCommands =
(nvidiaPlanHostPreparedCommandsS 0)
def phNoPreparation =
(lambda unrestricted tail : (family NativePhysicalCommands) . tail)
def nvidiaPlanHostCommandsOnS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(nvidiaPlanHostPreparedCommandsOnS session device phNoPreparation phNoPreparation)))
def nvidiaPlanHostCommandsOn =
(nvidiaPlanHostCommandsOnS 0)
def nvidiaPlanHostCommandsS =
(lambda unrestricted session : Nat .
(nvidiaPlanHostCommandsOnS session nvidiaDeviceZero))
def nvidiaPlanHostCommands =
(nvidiaPlanHostCommandsS 0)
-- The channel probe, Probe mode: the prelude alone, every status after the
-- root client's recorded and none asserted, then to stdout the status area
-- -- the 16-byte record per buffer, the UVM slots, the RM slots -- from the
-- state and the channel allocation's parameter block as the driver left it
-- (its `cid` word at 132 is the hardware channel identifier), then the root
-- freed. With a card it prints both and exits 0 whether or not the channel
-- came up; which call refused is read off the area.
def phProbeRecord : Nat =
(phBufferStatus 0)
def phProbeRecordExtent : Nat =
(naturalSaturatingSubtract (phBufferState 0) (phBufferStatus 0))
def phChannelParamsExtent : Nat =
368
def nvidiaPlanHostProbeCommandsOnS =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(phPipeCreate
(phPreludeOnS session
device
(constructor NvidiaPlanHostMode NvidiaPlanHostProbe)
layout
(phCall
phSysWrite
(phArgs3 (phImm 1) (phState phProbeRecord) (phImm phProbeRecordExtent))
b""
phDiscard
(phCall
phSysWrite
(phArgs3 (phImm 1) (phImm phChanP) (phImm phChannelParamsExtent))
b""
phDiscard
(phRelease
(phCall
phSysExitGroup
(phArgs3 (phImm 0) (phImm 0) (phImm 0))
b""
phDiscard
(phNext
(constructor NativePhysicalOperation NativePhysicalHaltSuccess)
(constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))))
def nvidiaPlanHostProbeCommandsOn =
(nvidiaPlanHostProbeCommandsOnS 0)
def nvidiaPlanHostProbeCommandsS =
(lambda unrestricted session : Nat .
(nvidiaPlanHostProbeCommandsOnS session nvidiaDeviceZero))
def nvidiaPlanHostProbeCommands =
(nvidiaPlanHostProbeCommandsS 0)
def phCommandCount =
(lambda unrestricted commands : (family NativePhysicalCommands) .
(eliminate
NativePhysicalCommands
(lambda unrestricted current : (family NativePhysicalCommands) . Nat)
commands
(branch NativePhysicalCommandsEnd . zero)
(branch NativePhysicalCommandsNext head tail induction . (succ induction))))
-- The number of assertions a command list carries: what a mode decides.
def phOperationIsAssert =
(lambda unrestricted operation : (family NativePhysicalOperation) .
(eliminate
NativePhysicalOperation
(lambda unrestricted current : (family NativePhysicalOperation) . Nat)
operation
(branch NativePhysicalSystemCall number argv payload result . 0)
(branch NativePhysicalCopyPayloadToState destination extent payload . 0)
(branch NativePhysicalMachineRoutine code argv result . 0)
(branch NativePhysicalFencePoll address expected polls . 0)
(branch NativePhysicalTelemetryAppend path record . 0)
(branch NativePhysicalAssertEqual left right error . 1)
(branch NativePhysicalAssertOneOf observed first second error . 1)
(branch NativePhysicalHaltSuccess . 0)
(branch NativePhysicalRepeatBegin count . 0)
(branch NativePhysicalSkipUnlessEqual left right count . 0)
(branch NativePhysicalRepeatEnd . 0)
(branch NativePhysicalRepeatEndWhen observed expected . 0)
(branch NativePhysicalStoreWord64 destination value . 0)
(branch NativePhysicalFenceWait address expected polls interval . 0)
(branch NativePhysicalRepeatBeginCounted count . 0)
(branch NativePhysicalAddWord64 destination left right . 0)
(branch NativePhysicalFloat64 operation destination left right . 0)))
def phCommandIsAssert =
(lambda unrestricted command : (family NativePhysicalCommand) .
(eliminate
NativePhysicalCommand
(lambda unrestricted current : (family NativePhysicalCommand) . Nat)
command
(branch NativePhysicalCommandValue operation identity . (phOperationIsAssert operation))))
def nvidiaPlanHostAssertionCount =
(lambda unrestricted commands : (family NativePhysicalCommands) .
(eliminate
NativePhysicalCommands
(lambda unrestricted current : (family NativePhysicalCommands) . Nat)
commands
(branch NativePhysicalCommandsEnd . zero)
(branch
NativePhysicalCommandsNext
head
tail
induction
.
(naturalAdd (phCommandIsAssert head) induction))))
-- the prelude alone under a mode, for the assertion contracts
def nvidiaPlanHostPreludeCommandsS =
(lambda unrestricted session : Nat .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(phPreludeS session mode layout (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))
def nvidiaPlanHostPreludeCommands =
(nvidiaPlanHostPreludeCommandsS 0)
def nvidiaPlanHostProgram =
(lambda unrestricted identity : Bytes .
(lambda unrestricted commands : (family NativePhysicalCommands) .
(constructor
NativePhysicalProgram
NativePhysicalProgramValue
(phWord phStateExtent)
(phWord phSlots)
commands
(phCommandCount commands)
identity
zero)))
def nvidiaPlanHostELF =
(lambda unrestricted identity : Bytes .
(lambda unrestricted commands : (family NativePhysicalCommands) .
(nativePhysicalGenerateNativeELFBytesDirect (nvidiaPlanHostProgram identity commands))))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.