Large source region · 4,065 lines
module Platform.Linux.Nvidia.PlanHost
import Data.Bytes
import Platform.Linux.Nvidia.DeviceBinding
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
family NvidiaPlanHostABI : Type 0
constructor NvidiaPlanHostABIValue
field unrestricted nvidiaPlanHostMapDMAIoctl : Nat
field unrestricted nvidiaPlanHostNVOS46Size : Nat
field unrestricted nvidiaPlanHostNVOS46DMAOffset : Nat
field unrestricted nvidiaPlanHostNVOS46Status : Nat
field unrestricted nvidiaPlanHostChannelClass : Nat
field unrestricted nvidiaPlanHostComputeClass : Nat
field unrestricted nvidiaPlanHostUsermodeClass : Nat
field unrestricted nvidiaPlanHostEngineType : Nat
-- the first four bytes of the driver version the ABI was built for,
-- little-endian ("580." is 0x2E303835): the host asks the driver for its
-- version before any card call and refuses another branch by name
field unrestricted nvidiaPlanHostDriverBranch : Nat
-- the bytes of NVA06C_CTRL_GPFIFO_SCHEDULE_PARAMS: 2 on the 570 branch
-- (bEnable, bSkipSubmit), 3 from 580 (bSkipEnable added); the wrong size is
-- NV_ERR_INVALID_ARGUMENT (0x1f), measured on an RTX A6000, 570.195.03
field unrestricted nvidiaPlanHostScheduleParamsSize : Nat
-- Required location of a separately allocated direct-RM USERD buffer.
-- Discrete Ampere needs video memory; the measured integrated GB10 path
-- uses system memory. This is target policy, not a runtime retry choice.
field unrestricted nvidiaPlanHostDirectUSERDMemory : (family NvidiaPlanHostMemory)
field unrestricted nvidiaPlanHostDirectChannelFlags : Nat
-- Direct-RM cache snooping is target policy. The GB10 bring-up's host-cached
-- system buffers use 0x8010; the qualified Ampere path keeps 0x8000. See
-- Memory.ABI.memoryABIDMAMappingFlags. A CPU publication barrier alone does
-- not make a non-snooping GPU mapping coherent with cached CPU writes.
field unrestricted nvidiaPlanHostDirectDMAFlags : Nat
end-family
-- one upload: bytes, or the contents of a file at run time
family NvidiaPlanHostFills : Type 0
constructor NvidiaPlanHostFillsEnd
constructor NvidiaPlanHostFillBytes
field unrestricted nvidiaPlanHostFillHost : Nat
field unrestricted nvidiaPlanHostFillPayload : Bytes
recursive unrestricted nvidiaPlanHostFillsTail
constructor NvidiaPlanHostFillFile
field unrestricted nvidiaPlanHostFillFileHost : Nat
field unrestricted nvidiaPlanHostFillFilePath : Bytes
field unrestricted nvidiaPlanHostFillFileExtent : Nat
recursive unrestricted nvidiaPlanHostFillFileTail
end-family
-- one readback: a host range written to stdout after completion
family NvidiaPlanHostReads : Type 0
constructor NvidiaPlanHostReadsEnd
constructor NvidiaPlanHostReadsNext
field unrestricted nvidiaPlanHostReadHost : Nat
field unrestricted nvidiaPlanHostReadExtent : Nat
recursive unrestricted nvidiaPlanHostReadsTail
end-family
family NvidiaPlanHostLifecycle : Type 0
constructor NvidiaPlanHostDirectRM
-- 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 570 branch: the 56-byte NVOS46 (the layout the retired 575 ABI of
-- the RTX 3070 fixtures used) and the 2-byte schedule parameters. The 575
-- branch is no longer offered for any sm_86 card on RunPod (2026-09-24:
-- 570.195, 580.65 .. 580.178, 595.91), so its ABI could not be qualified
-- again and was retired; this one is qualified on an RTX A6000, 570.195.03.
def nvidiaPlanHostAmpere570 : (family NvidiaPlanHostABI) =
(constructor
NvidiaPlanHostABI
NvidiaPlanHostABIValue
0xC0384657
56
40
48
0xC56F
0xC7C0
0xC561
0
0x2E303735
2
(constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)
0x01000000
0x8000)
def nvidiaPlanHostAmpere580 : (family NvidiaPlanHostABI) =
(constructor
NvidiaPlanHostABI
NvidiaPlanHostABIValue
0xC0404657
64
48
56
0xC56F
0xC7C0
0xC561
0
0x2E303835
3
(constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)
0x01000000
0x8000)
-- The H100 SXM (compute 9.0) on the 580 branch: the Ampere 580 ABI with
-- 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.
def nvidiaPlanHostHopper580 : (family NvidiaPlanHostABI) =
(constructor NvidiaPlanHostABI NvidiaPlanHostABIValue 0xC0404657 64 48 56 0xC86F 0xCBC0 0xC661 0 0x2E303835 3
(constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory) 0x01000000 0x8000)
-- The DGX Spark's GB10 (compute 12.1) on the 580 branch: the 580 DMA-map ABI
-- above with the classes this GPU's class list offers and the ladder
-- allocated (tools/dgx/rung_tsg.py, rung_execute.py): BLACKWELL_CHANNEL_GPFIFO_A
-- 0xC96F, BLACKWELL_COMPUTE_B 0xCEC0, HOPPER_USERMODE_A 0xC661.
def nvidiaPlanHostBlackwell580 : (family NvidiaPlanHostABI) =
(constructor
NvidiaPlanHostABI
NvidiaPlanHostABIValue
0xC0404657
64
48
56
0xC96F
0xCEC0
0xC661
0
0x2E303835
3
-- USERD in system memory (the GB10's channel buffers, Coppelius.Build.
-- NativeHost), the channel flags every UVM plan allocates with, and the
-- direct-RM DMA flags, which a UVM plan never reads
(constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)
0x01000000
0x8000)
-- A layout built for another driver ABI: every buffer, the lifecycle and
-- the expected card unchanged, only the ABI (the DMA-map parameters, the
-- classes, the driver branch it demands) replaced.
def nvidiaPlanHostWithABI =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family NvidiaPlanHostLayout))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
previous
lifecycle
expectedName
errorHost
.
(constructor
NvidiaPlanHostLayout
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost)))))
-- 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 phSysMmap : Nat =
9
def phSysIoctl : Nat =
16
def phSysDup2 : Nat =
33
def phSysExitGroup : Nat =
231
def phSysOpenat : Nat =
257
def phSysPipe2 : Nat =
293
def phAtFdCwd : Nat =
18446744073709551516
def phOpenFlags : Nat =
0x80002
def phMapAnonymousFixed : Nat =
0x32
def phMapSharedFixed : Nat =
0x11
def phNoDescriptor : Nat =
18446744073709551615
-- RM and UVM escapes
def phRMAlloc : Nat =
0xC020462B
def phRMControl : Nat =
0xC020462A
def phRMMapMemory : Nat =
0xC038464E
def phRMFree : Nat =
0xC0104629
def phRegisterFD : Nat =
0xC00446C9
def phWaitOpen : Nat =
0xC00846DA
def phUVMInitialize : Nat =
0x30000001
def phUVMMMInitialize : Nat =
75
def phUVMRegisterGPU : Nat =
37
def phUVMRegisterGPUVASpace : Nat =
25
def phUVMRegisterChannel : Nat =
27
def phUVMCreateExternalRange : Nat =
73
def phUVMMapExternalAllocation : Nat =
33
def phUVMChannelRangeBase : Nat =
0xA00000000
def phUVMChannelRangeExtent : Nat =
0x4000000
-- result slots and fixed descriptors
def phSlotControl : Nat =
0
def phSlotGPU : Nat =
1
def phSlotMap : Nat =
2
def phSlotFile : Nat =
3
-- slots 4..13 belong to the request host (PlanHostRequest), 14 and 15 to
-- the native telemetry. Transfers own the next slot and never overwrite a
-- request file descriptor or a mapping result while checking short I/O.
def phSlotTransfer : Nat =
16
def phSlots : Nat =
(succ phSlotTransfer)
def phFdControl : Nat =
100
def phFdCard : Nat =
101
def phFdMap : Nat =
102
def phFdUVM : Nat =
103
def phFdUVMMemoryMap : Nat =
104
-- RM handles, caller-chosen for children
def phHDevice : Nat =
0xDEAD0080
def phHSubdevice : Nat =
0xDEAD2080
def phHVASpace : Nat =
0xDEAD90F1
def phHError : Nat =
0xDEAD0E44
def phHGroup : Nat =
0xDEADA06C
def phHContext : Nat =
0xDEAD9067
def phHDMA : Nat =
0xDEAD0070
def phHMemory =
(lambda unrestricted index : Nat . (naturalAdd 0xB0000000 index))
def phHVirtual =
(lambda unrestricted index : Nat . (naturalAdd 0xB1000000 index))
def phHClass =
(lambda unrestricted class : Nat . (naturalAdd 0xDEAD0000 class))
-- state layout, 16 KiB: RM call blocks, then a 16-byte status record per
-- buffer, then 256 bytes of call blocks per buffer (at most 24 buffers, to
-- 10240); the request host's areas follow (PlanHostRequest)
def phStateExtent : Nat =
16384
def phBufferBlocksEnd : Nat =
10240
def phRoot : Nat =
0
def phDev : Nat =
64
def phSub : Nat =
128
def phVAS : Nat =
192
def phErrMap : Nat =
256
def phErr : Nat =
2048
def phGroup : Nat =
2112
def phCtx : Nat =
2176
def phChan : Nat =
2240
def phComp : Nat =
2304
def phUser : Nat =
2368
def phBind : Nat =
2432
def phSched : Nat =
2496
def phTok : Nat =
2560
def phDoorMap : Nat =
2624
def phWait : Nat =
2688
def phPipe : Nat =
2752
def phScratch : Nat =
2816
def phName : Nat =
2880
def phPreempt : Nat =
3008
def phFree : Nat =
3040
def phDMAObject : Nat =
3072
def phUVMControl : Nat =
3136
def phBufferState =
(lambda unrestricted index : Nat . (naturalAdd 4096 (naturalMultiply index 256)))
def phBufferStatus =
(lambda unrestricted index : Nat . (naturalAdd 3200 (naturalMultiply index 16)))
def phBuffersMaximum : Nat =
24
-- the fixed anonymous parameter page, 64 KiB
-- 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 phTokP : Nat =
0x50001800
def phRegFdP : Nat =
0x50001980
def phPreemptP : Nat =
0x50001A00
def phNameP : Nat =
0x50001B00
def phMemP =
(lambda unrestricted index : Nat . (naturalAdd 0x50002000 (naturalMultiply index 0x200)))
def phVirtP =
(lambda unrestricted index : Nat . (naturalAdd 0x50002100 (naturalMultiply index 0x200)))
def phDMAObjectP : Nat =
0x50007F00
def phUVMGidP : Nat =
0x50008000
def phUVMInitP : Nat =
0x50008200
def phUVMMMP : Nat =
0x50008300
def phUVMRegisterGPUP : Nat =
0x50008400
def phUVMRegisterVASpaceP : Nat =
0x50008500
def phUVMRegisterChannelP : Nat =
0x50008600
def phUVMCreateRangeP : Nat =
0x50008700
def phUVMMapAllocationP : Nat =
0x50009000
def phDoorHost : Nat =
0x60800000
def phStatusSentinel : Nat =
0xFFFFFFFF
-- ---- little-endian blocks ----
def phZeros =
(lambda unrestricted count : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
b""
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
count))
def phDrop =
dataBytesDropValidated
def phTake =
dataBytesTakeValidated
def phW32 =
(lambda unrestricted value : Nat . (dataBytesWord32LE (modelWord32FromNaturalTruncated value)))
def phW64 =
(lambda unrestricted value : Nat . (dataBytesWord64LE (phWord value)))
def phSet =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted field : Bytes .
(bytes-append
(phTake offset block)
(bytes-append field (phDrop (naturalAdd offset (bytes-length field)) block))))))
def phSet32 =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted value : Nat . (phSet block offset (phW32 value)))))
def phSet64 =
(lambda unrestricted block : Bytes .
(lambda unrestricted offset : Nat .
(lambda unrestricted value : Nat . (phSet block offset (phW64 value)))))
-- ---- the pipe memcpy ----
def phCopyStateToState =
(lambda unrestricted destination : Nat .
(lambda unrestricted source : Nat .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysWrite
(phArgs3 (phLoad (naturalAdd phPipe 4)) (phState source) (phImm count))
b""
phDiscard
(phCall
phSysRead
(phArgs3 (phLoad phPipe) (phState destination) (phImm count))
b""
phDiscard
tail))))))
-- A pipe is not an unbounded staging buffer. A single-threaded write/read
-- pair deadlocks when its write exceeds capacity (the matrix qualification
-- stopped in write(901120), after filling 65536 bytes). Drain every bounded
-- chunk before writing another. Linux PIPE_BUF is 4096 on both target ABIs;
-- the empty pipe admits that atomic extent even when capacity is one page.
-- Short/error returns fail by name, including interruption; no partial copy
-- is reported as a successful upload. Result slot ownership is explicit.
def phPipeChunkBytes : Nat =
4096
def phPipeChunkCount =
(lambda unrestricted count : Nat .
(naturalAdd
(naturalDivideUnchecked count phPipeChunkBytes)
(naturalNonzero (naturalModuloUnchecked count phPipeChunkBytes))))
def phPipeChunk =
(lambda unrestricted source : (family NativePhysicalOperand) .
(lambda unrestricted destination : (family NativePhysicalOperand) .
(lambda unrestricted count : Nat .
(lambda unrestricted payload : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysWrite
(phArgs3 (phLoad (naturalAdd phPipe 4)) source (phImm count))
payload
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm count)
b"pipe-copy-write"
(phCall
phSysRead
(phArgs3 (phLoad phPipe) destination (phImm count))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm count)
b"pipe-copy-read"
tail)))))))))
def phFill =
(lambda unrestricted address : Nat .
(lambda unrestricted payload : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(nat-eliminate
(lambda unrestricted remaining : Nat .
(pi unrestricted at : Nat .
(pi unrestricted bytes : Bytes . (family NativePhysicalCommands))))
(lambda unrestricted at : Nat . (lambda unrestricted bytes : Bytes . tail))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (pi unrestricted at : Nat . (pi unrestricted bytes : Bytes . (family NativePhysicalCommands))) .
(lambda unrestricted at : Nat .
(lambda unrestricted bytes : Bytes .
(let unrestricted count =
(naturalMinimum phPipeChunkBytes (bytes-length bytes))
in
(phPipeChunk
phPayload
(phImm at)
count
(dataBytesTakeValidated count bytes)
(induction (naturalAdd at count) (dataBytesDropValidated count bytes))))))))
(phPipeChunkCount (bytes-length payload)))
address
payload))))
-- Address-based copies share the same transfer/check mechanism. Their
-- ranges must be disjoint as before; this is not an overlapping memmove.
def phPipeRanges =
(lambda unrestricted source : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
(lambda unrestricted destination : (pi unrestricted offset : Nat . (family NativePhysicalOperand)) .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted chunks =
(phPipeChunkCount count)
in
(nat-eliminate
(lambda unrestricted i : Nat . (family NativePhysicalCommands))
tail
(lambda unrestricted index : Nat .
(lambda unrestricted rest : (family NativePhysicalCommands) .
(let unrestricted offset =
(naturalMultiply
(naturalSaturatingSubtract chunks (succ index))
phPipeChunkBytes)
in
(phPipeChunk
(source offset)
(destination offset)
(naturalMinimum phPipeChunkBytes (naturalSaturatingSubtract count offset))
b""
rest))))
chunks))))))
def phCopyMappedToState =
(lambda unrestricted address : Nat .
(lambda unrestricted destination : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phImm (naturalAdd address offset)))
(lambda unrestricted offset : Nat . (phState (naturalAdd destination offset))))))
def phCopyStateToMapped =
(lambda unrestricted source : Nat .
(lambda unrestricted address : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phState (naturalAdd source offset)))
(lambda unrestricted offset : Nat . (phImm (naturalAdd address offset))))))
def phCopyMappedToMapped =
(lambda unrestricted source : Nat .
(lambda unrestricted destination : Nat .
(phPipeRanges
(lambda unrestricted offset : Nat . (phImm (naturalAdd source offset)))
(lambda unrestricted offset : Nat . (phImm (naturalAdd destination offset))))))
-- the pipe the memcpys above go through; every entry point creates it first
def phPipeCreate =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall phSysPipe2 (phArgs3 (phState phPipe) (phImm 0) (phImm 0)) b"" phDiscard tail))
-- Read the declared prefix into a mapped buffer. Short reads (including
-- interruption), missing files and I/O errors fail before later uploads or
-- submissions; an unread suffix is allowed by this fill's prefix contract.
-- Keep the descriptor in phScratch while phSlotFile carries read/close
-- results. Both are owned temporaries across this straight-line fragment;
-- no caller's request or telemetry slot is borrowed. Closing also prevents
-- a multi-tensor import from exhausting the process's file descriptors.
-- Bytes has an explicit extent; openat requires a terminating zero. An
-- eight-byte path otherwise runs into the next payload in the host image.
-- Caller-supplied trailing zeros remain harmless; never rely on pool padding.
def phReadFile =
(lambda unrestricted path : Bytes .
(lambda unrestricted address : Nat .
(lambda unrestricted count : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm 0))
(bytes-append path b"\x00")
(phStore phSlotFile)
(phNext
(constructor
NativePhysicalOperation
NativePhysicalStoreWord64
(phState phScratch)
(phSlot phSlotFile))
(phCall
phSysRead
(phArgs3 (phSlot phSlotFile) (phImm address) (phImm count))
b""
(phStore phSlotFile)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotFile)
(phImm count)
b"input-file-read"
(phCall
phSysClose
(phArgs3 (phLoad phScratch) (phImm 0) (phImm 0))
b""
(phStore phSlotFile)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotFile)
(phImm 0)
b"input-file-close"
tail))))))))))
def phRangeBase =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM 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
mapDMA
size
dmaOffset
status
channel
compute
usermode
engine
driverBranch
scheduleSize
userdMemory
channelFlags
directDMAFlags
.
(naturalSelect
(naturalEqual which 0)
mapDMA
(naturalSelect
(naturalEqual which 1)
size
(naturalSelect
(naturalEqual which 2)
dmaOffset
(naturalSelect
(naturalEqual which 3)
status
(naturalSelect
(naturalEqual which 4)
channel
(naturalSelect
(naturalEqual which 5)
compute
(naturalSelect
(naturalEqual which 6)
usermode
(naturalSelect
(naturalEqual which 7)
engine
(naturalSelect
(naturalEqual which 8)
driverBranch
(naturalSelect (naturalEqual which 9) scheduleSize channelFlags))))))))))))))
def phUSERDRequiresVideo =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . Nat)
abi
(branch
NvidiaPlanHostABIValue
mapDMA
size
dmaOffset
status
channel
compute
usermode
engine
driverBranch
scheduleSize
userdMemory
channelFlags
directDMAFlags
.
(eliminate
NvidiaPlanHostMemory
(lambda unrestricted memory : (family NvidiaPlanHostMemory) . Nat)
userdMemory
(branch NvidiaPlanHostSystemMemory . 0)
(branch NvidiaPlanHostVideoMemory . 1)
(branch NvidiaPlanHostPagedSystemMemory . 0)
(branch NvidiaPlanHostGPUCachedSystemMemory . 0)))))
def phIsUVM =
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) . Nat)
lifecycle
(branch NvidiaPlanHostDirectRM 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))
-- 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 phHostResidents =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted extras : (family ArenaResidents) .
(phEachResident
phHostResident
(phAllocatedBuffers layout)
(phResident
b"parameters"
phParams
nvidiaPlanHostParameterMappingBytes
(phResident
b"doorbell"
phDoorHost
0x10000
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) .
(family ArenaResidents))
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(nat-eliminate
(lambda unrestricted current : Nat . (family ArenaResidents))
extras
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family ArenaResidents) .
(phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes extras)))
(naturalNonzero errorHost)))))))))
-- [inner, inner + innerExtent) inside [outer, outer + outerExtent)
def phInside =
(lambda unrestricted inner : Nat .
(lambda unrestricted innerExtent : Nat .
(lambda unrestricted outer : Nat .
(lambda unrestricted outerExtent : Nat .
(naturalAnd
(naturalLessOrEqual outer inner)
(naturalLessOrEqual (naturalAdd inner innerExtent) (naturalAdd outer outerExtent)))))))
-- under UVM, the USERD entry inside the GPFIFO buffer in both spaces
def phUSERDAliasInside =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat)
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(naturalSelect
(phIsUVM lifecycle)
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
userd
(branch
NvidiaPlanHostBufferValue
aliasIdentity
aliasGPU
aliasHost
aliasExtent
aliasMemory
.
(eliminate
NvidiaPlanHostBuffer
(lambda unrestricted current : (family NvidiaPlanHostBuffer) . Nat)
gpfifo
(branch
NvidiaPlanHostBufferValue
identity
gpu
host
extent
memory
.
(naturalAnd
(phInside aliasGPU aliasExtent gpu extent)
(phInside aliasHost aliasExtent host extent))))))
1))))
-- 1 when the layout's placement is certified in both spaces
def nvidiaPlanHostLayoutCertified =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted extras : (family ArenaResidents) .
(naturalAnd
(arenaCertificate phGPUSpaceBytes (phGPUResidents layout))
(naturalAnd
(arenaCertificate phHostSpaceBytes (phHostResidents layout extras))
(phUSERDAliasInside layout)))))
-- Every upload lands inside a host-mapped buffer of the layout: bytes, or a
-- file's declared extent. The subagent's RTX 3070 sweep (2026-09-23) found
-- program tables up to 7936 bytes built into a 4096-byte program buffer and
-- copied past it at run time -- the kernel never ran; now the build refuses.
def nvidiaPlanHostFillsAdmitted =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(eliminate
NvidiaPlanHostFills
(lambda unrestricted current : (family NvidiaPlanHostFills) . Nat)
fills
(branch NvidiaPlanHostFillsEnd . 1)
(branch
NvidiaPlanHostFillBytes
host
payload
rest
induction
.
(naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction))
(branch
NvidiaPlanHostFillFile
host
path
extent
rest
induction
.
(naturalAnd (nvidiaPlanHostContains layout host extent) induction)))))
-- what a plan-derived host needs admitted before it is built
def nvidiaPlanHostAdmitted =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted fills : (family NvidiaPlanHostFills) .
(naturalAnd
(nvidiaPlanHostLayoutAdmitted layout)
(naturalAnd
(nvidiaPlanHostLayoutCertified layout (constructor ArenaResidents ArenaResidentsEnd))
(nvidiaPlanHostFillsAdmitted layout fills)))))
-- system memory: host-cached, contiguous or noncontiguous as declared. video memory: the local-user
-- object, write-combined, contiguous, page-aligned.
-- system memory's attributes: PCI, cached, and contiguous (0x32000000) or,
-- paged, non-contiguous (0x2A000000)
def phGPUCachedPageBytes : Nat =
0x10000
-- NV_MEMORY_ALLOCATION_PARAMS for a buffer: owner, flags (8), attr (24),
-- attr2 (28), format (32), size (64), alignment (72), limit (88)
def phGPUCachedMemoryParams =
(lambda unrestricted extent : Nat .
(phSet64
(phSet64
(phSet64
(phSet32
(phSet32
(phSet32 (phSet32 (phSet32 (phZeros 128) 0 0x636c6161) 8 0x0000C001) 24 0x0B000000)
28
0x00000005)
32
0x00000006)
64
extent)
72
phGPUCachedPageBytes)
88
(naturalSaturatingSubtract extent 1)))
def phMemoryParams =
(lambda unrestricted video : Nat .
(lambda unrestricted paged : Nat .
(lambda unrestricted cached : Nat .
(lambda unrestricted inside : Nat .
(lambda unrestricted extent : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(phSet64
(phSet32
(phSet32 (phZeros 128) 0 0x636c6161)
24
(naturalSelect paged 0x2A000000 0x32000000))
64
extent)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes . (phGPUCachedMemoryParams extent)))
cached)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes .
(phSet64
(phSet64
(phSet32
(phSet32 (phSet32 (phZeros 128) 0 0x48454C49) 8 0x00008000)
24
(naturalSelect inside 0x58000000 0x50000000))
64
extent)
72
0x1000)))
video))))))
def phMemoryClass =
(lambda unrestricted video : Nat . (naturalSelect video 0x40 0x3E))
-- the host mapping of one buffer through a fresh control descriptor, or for
-- video memory through a fresh card descriptor
-- 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 phMapMemory =
(lambda unrestricted identity : Bytes .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted block : Nat .
(lambda unrestricted hMemory : Nat .
(lambda unrestricted video : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted host : Nat .
(lambda unrestricted statusOffset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted flags =
(naturalSelect video 0x01010000 0x03008000)
in
(phMappingDescriptor
video
(phCall
phSysIoctl
(phArgs3 (phImm phFdMap) (phImm phRegisterFD) (phImm phRegFdP))
b""
phDiscard
(phCopy
block
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32 (phSet32 (phZeros 56) 4 phHDevice) 8 hMemory)
24
extent)
40
phStatusSentinel)
44
flags)
48
phFdMap)
(phCopyStateToState
block
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState block))
b""
phDiscard
(phCopyStateToState
statusOffset
(naturalAdd block 40)
4
(phCheckStateZero32
identity
(phTolerate mode)
(naturalAdd block 40)
(phCall
phSysMmap
(phArgs
(phImm host)
(phImm extent)
(phImm 3)
(phImm phMapSharedFixed)
(phImm phFdMap)
(phImm 0))
b""
phDiscard
tail))))))))))))))))))
def phHostMap =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phMapMemory
b"host-map"
mode
(naturalAdd (phBufferState index) 128)
(phHMemory index)
(phBufferIsVideo buffer)
(phBufferExtent buffer)
(phBufferHost buffer)
(naturalAdd (phBufferStatus index) 12)
tail)))))
def phDirectDMAFlags =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(eliminate
NvidiaPlanHostABI
(lambda unrestricted current : (family NvidiaPlanHostABI) . Nat)
abi
(branch
NvidiaPlanHostABIValue
mapDMA
size
dmaOffset
status
channel
compute
usermode
engine
driverBranch
scheduleSize
userdMemory
channelFlags
directDMAFlags
.
directDMAFlags)))
-- direct-RM: a fixed virtual reservation and the DMA map to it
def phDirectRange =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted st =
(phBufferState index)
in
(let unrestricted gpu =
(phBufferGPU buffer)
in
(let unrestricted extent =
(phBufferExtent buffer)
in
(phFill
(phVirtP index)
(phSet32
(phSet64
(phSet64 (phZeros 24) 0 gpu)
8
(naturalSaturatingSubtract (naturalAdd gpu extent) 1))
16
phHVASpace)
(phAlloc
b"alloc:virtual"
(phTolerate mode)
(naturalAdd st 32)
phHDevice
0x70
(phVirtP index)
24
(phHVirtual index)
(naturalAdd (phBufferStatus index) 4)
(phCopy
(naturalAdd st 64)
(phSet32
(phSet64
(phSet64
(phSet32
(phSet32
(phSet32
(phSet32 (phZeros (phABI abi 1)) 4 phHDevice)
8
(phHVirtual index))
12
(phHMemory index))
32
(phDirectDMAFlags abi))
24
extent)
(phABI abi 2)
gpu)
(phABI abi 3)
phStatusSentinel)
(phCopyStateToState
(naturalAdd st 64)
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3
(phSlot phSlotControl)
(phImm (phABI abi 0))
(phState (naturalAdd st 64)))
b""
phDiscard
(phCopyStateToState
(naturalAdd (phBufferStatus index) 8)
(naturalAdd st (naturalAdd 64 (phABI abi 3)))
4
(phCheckStateZero32
b"dma-map"
(phTolerate mode)
(naturalAdd st (naturalAdd 64 (phABI abi 3)))
tail)))))))))))))))
-- NVOS46 flags of the UVM path's DMA map: DMA_OFFSET_FIXED, CACHE_SNOOP,
-- and 4 KiB pages; a GPU-cached buffer takes the allocation's own (64 KiB)
-- page size instead
def phUVMDMAFlags : Nat =
0x8110
def phUVMDMAFlagsDefaultPages : Nat =
0x8010
-- UVM: an external range at the plan's address, the DMA map through the
-- device DMA selector, and the mapping registered with UVM
def phUVMRange =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted inside : Nat .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted st =
(phBufferState index)
in
(let unrestricted gpu =
(phBufferGPU buffer)
in
(let unrestricted extent =
(phBufferExtent buffer)
in
(let unrestricted tolerate =
(phTolerate mode)
in
(phWhen
(naturalIsZero inside)
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phFill
phUVMCreateRangeP
(phSet32
(phSet64 (phSet64 (phZeros 24) 0 gpu) 8 extent)
16
phStatusSentinel)
(phUVMCall
b"uvm-buffer-range"
(naturalAdd 8 (naturalMultiply 2 index))
tolerate
phFdUVM
phUVMCreateExternalRange
phUVMCreateRangeP
16
rest)))
(phCopy
(naturalAdd st 64)
(phSet32
(phSet64
(phSet64
(phSet32
(phSet32
(phSet32 (phSet32 (phZeros (phABI abi 1)) 4 phHDevice) 8 phHDMA)
12
(phHMemory index))
32
(naturalSelect
(phBufferIsGPUCached buffer)
phUVMDMAFlagsDefaultPages
phUVMDMAFlags))
24
extent)
(phABI abi 2)
gpu)
(phABI abi 3)
phStatusSentinel)
(phCopyStateToState
(naturalAdd st 64)
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3
(phSlot phSlotControl)
(phImm (phABI abi 0))
(phState (naturalAdd st 64)))
b""
phDiscard
(phCopyStateToState
(naturalAdd (phBufferStatus index) 8)
(naturalAdd st (naturalAdd 64 (phABI abi 3)))
4
(phCheckStateZero32
b"dma-map-uvm"
tolerate
(naturalAdd st (naturalAdd 64 (phABI abi 3)))
(phFill
phUVMMapAllocationP
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32
(phSet64 (phSet64 (phZeros 9264) 0 gpu) 8 extent)
40
1)
9240
1)
9248
phFdControl)
9256
(phHMemory index))
9260
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
(naturalAdd phUVMMapAllocationP 24)
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMMapAllocationP 9252)
4
(phUVMCall
b"uvm-buffer-map"
(naturalAdd 9 (naturalMultiply 2 index))
tolerate
phFdUVM
phUVMMapExternalAllocation
phUVMMapAllocationP
9260
tail))))))))))))))))))))
-- One buffer: allocate, place, map.
def phBuffer =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted index : Nat .
(lambda unrestricted buffer : (family NvidiaPlanHostBuffer) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted video =
(phBufferIsVideo buffer)
in
(let unrestricted uvm =
(phIsUVM lifecycle)
in
(let unrestricted inside =
(phInsideRange lifecycle (phBufferGPU buffer) (phBufferExtent buffer))
in
(phFill
(phMemP index)
(phMemoryParams
video
(phBufferIsPaged buffer)
(phBufferIsGPUCached buffer)
inside
(phBufferExtent buffer))
(phAlloc
(bytes-append b"alloc:" (phBufferIdentity buffer))
(phTolerate mode)
(phBufferState index)
phHDevice
(phMemoryClass video)
(phMemP index)
128
(phHMemory index)
(phBufferStatus index)
(phWhen
(naturalIsZero uvm)
(phDirectRange abi mode index buffer)
(phWhen
uvm
(phUVMRange abi mode inside index buffer)
(phWhen
(naturalNonzero (phBufferHost buffer))
(phHostMap mode index buffer)
tail))))))))))))))
def phDataBuffers =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted first : Nat .
(lambda unrestricted buffers : (family NvidiaPlanHostBuffers) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(eliminate
NvidiaPlanHostBuffers
(lambda unrestricted current : (family NvidiaPlanHostBuffers) .
(pi unrestricted index : Nat . (family NativePhysicalCommands)))
buffers
(branch NvidiaPlanHostBuffersEnd . (lambda unrestricted index : Nat . tail))
(branch
NvidiaPlanHostBuffersNext
head
rest
induction
.
(lambda unrestricted index : Nat .
(phBuffer abi mode lifecycle index head (induction (succ index))))))
first)))))))
-- ---- device discovery ----
-- 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 phOpenSelectedCard =
(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 phFdCard) (phImm 0))
b""
(phStore phSlotTransfer)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTransfer)
(phImm phFdCard)
b"card-descriptor"
tail))))))))))))
-- 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 phBindSelectedDevice =
(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
phHDevice
(phRMStatusSlot 13)
tail)))))))))))))))
-- 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.
def phNameWord =
(phCompareMappedWord phIdentity (naturalAdd phNameP 4))
def phExpectName =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted expected : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phNameP
(phZeros 132)
(phControl
b"control:phName"
(phTolerate mode)
(phRMStatusSlot 11)
phName
phHSubdevice
0x20800110
phNameP
132
(phNameWord
expected
0
(phNameWord
expected
8
(phNameWord
expected
16
(phNameWord
expected
24
(phNameWord
expected
32
(phNameWord
expected
40
(phNameWord expected 48 (phNameWord expected 56 tail)))))))))))))
def phExpectDeviceUUID =
(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
phHSubdevice
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))))))))))
-- ---- the UVM driver ----
def phUVMPrepare =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted base : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phUVMGidP
(phSet32 (phSet32 (phZeros 268) 4 2) 8 16)
(phControl
b"control:phUVMControl"
(phTolerate mode)
(phRMStatusSlot 12)
phUVMControl
phHSubdevice
0x2080014A
phUVMGidP
268
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags))
b"/dev/nvidia-uvm\x00"
(phStore phSlotMap)
(phCall
phSysDup2
(phArgs3 (phSlot phSlotMap) (phImm phFdUVM) (phImm 0))
b""
(phStore phSlotMap)
(phFill
phUVMInitP
(phSet32 (phZeros 16) 8 phStatusSentinel)
(phUVMCallAfterOpen
(phTolerate mode)
b"uvm-initialize"
1
(phTolerate mode)
phFdUVM
phUVMInitialize
phUVMInitP
8
(phCall
phSysOpenat
(phArgs3 (phImm phAtFdCwd) phPayload (phImm phOpenFlags))
b"/dev/nvidia-uvm\x00"
(phStore phSlotMap)
(phCall
phSysDup2
(phArgs3 (phSlot phSlotMap) (phImm phFdUVMMemoryMap) (phImm 0))
b""
(phStore phSlotMap)
(phFill
phUVMMMP
(phSet32 (phSet32 (phZeros 8) 0 phFdUVM) 4 phStatusSentinel)
(phUVMCallAfterOpen
(phTolerate mode)
b"uvm-mm-initialize"
2
1
phFdUVMMemoryMap
phUVMMMInitialize
phUVMMMP
4
(phFill
phUVMRegisterGPUP
(phSet32
(phSet32 (phZeros 40) 24 phStatusSentinel)
36
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterGPUP
16
(phUVMCall
b"uvm-register-gpu"
3
(phTolerate mode)
phFdUVM
phUVMRegisterGPU
phUVMRegisterGPUP
36
(phFill
phUVMRegisterVASpaceP
(phSet32
(phSet32
(phSet32 (phZeros 32) 16 phFdControl)
24
phHVASpace)
28
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterVASpaceP
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMRegisterVASpaceP 20)
4
(phUVMCall
b"uvm-register-vaspace"
4
(phTolerate mode)
phFdUVM
phUVMRegisterGPUVASpace
phUVMRegisterVASpaceP
28
(phWhen
(naturalNonzero extent)
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phFill
phUVMCreateRangeP
(phSet32
(phSet64 (phSet64 (phZeros 24) 0 base) 8 extent)
16
phStatusSentinel)
(phUVMCall
b"uvm-external-range"
6
(phTolerate mode)
phFdUVM
phUVMCreateExternalRange
phUVMCreateRangeP
16
rest)))
tail))))))))))))))))))))))
def phUVMRegisterChannelCommands =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phUVMRegisterChannelP
(phSet32
(phSet64
(phSet64
(phSet32 (phSet32 (phZeros 56) 16 phFdControl) 24 (phHClass (phABI abi 4)))
32
phUVMChannelRangeBase)
40
phUVMChannelRangeExtent)
48
phStatusSentinel)
(phCopyMappedToMapped
(naturalAdd phUVMGidP 12)
phUVMRegisterChannelP
16
(phCopyStateToMapped
(naturalAdd phRoot 8)
(naturalAdd phUVMRegisterChannelP 20)
4
(phUVMCall
b"uvm-register-channel"
5
(phTolerate mode)
phFdUVM
phUVMRegisterChannel
phUVMRegisterChannelP
48
tail)))))))
-- ---- publishing a submission ----
-- gpPut into USERD, SFENCE, the work-submit token into the doorbell: the
-- training runtime's publication routine (x86: mov [rdi], esi; sfence;
-- mov [rdx], ecx), run on this thread, so the doorbell cannot reach the card
-- ahead of gpPut through a write-combining buffer. The token is loaded
-- from the parameter page into the scratch word first.
--
-- Measured on an RTX 3090, driver 580.178.04, 2026-09-24. Before, gpPut
-- went through the pipe copy and the doorbell after it, unordered: 7 hangs
-- in 250 warp-sum runs, and in every one the semaphores were untouched (the
-- device never began the pushbuffer), USERD's GP_PUT 1 and GP_GET 0 (the
-- channel never fetched the entry) -- the doorbell had arrived before
-- gpPut. A membarrier between the two (a locked-instruction barrier, which
-- need not drain write-combining buffers) did not help: 11 hangs in 300
-- against 6 unfenced. This routine: 0 hangs in 300 against 13 unfenced,
-- interleaved on the same card.
def phPublishCode : Bytes =
(eliminate
X86NativeAssemblyResult
(lambda unrestricted current : (family X86NativeAssemblyResult) . Bytes)
nativePhysicalTrainingGeneratePublish32Routine
(branch X86NativeAssemblyEncoded code . code)
(branch X86NativeAssemblyEncodeDuplicateLabel name . b"")
(branch X86NativeAssemblyEncodeOffsetOverflow . b"")
(branch X86NativeAssemblyMissingLabel name . b"")
(branch X86NativeAssemblyDisplacementOutOfRange name . b""))
def phLoadToken =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy phScratch (phZeros 8) (phCopyMappedToState phTokP phScratch 4 tail)))
def phPublishOperand =
(lambda unrestricted userdGPPut : Nat .
(lambda unrestricted gpPut : (family NativePhysicalOperand) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor
NativePhysicalOperation
NativePhysicalMachineRoutine
phPublishCode
(phArgs
(phImm userdGPPut)
gpPut
(phImm (naturalAdd phDoorHost 0x90))
(phLoad phScratch)
(phImm 0)
(phImm 0))
phDiscard)
tail))))
def phPublish =
(lambda unrestricted userdGPPut : Nat .
(lambda unrestricted gpPut : Nat . (phPublishOperand userdGPPut (phImm gpPut))))
-- ---- the doorbell ----
def phDoorbell =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysIoctl
(phArgs3 (phImm phFdCard) (phImm phRegisterFD) (phImm phRegFdP))
b""
phDiscard
(phCopy
phDoorMap
(phSet32
(phSet32
(phSet32
(phSet64
(phSet32 (phSet32 (phZeros 56) 4 phHSubdevice) 8 (phHClass (phABI abi 6)))
24
0x10000)
40
phStatusSentinel)
44
0)
48
phFdCard)
(phCopyStateToState
phDoorMap
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMMapMemory) (phState phDoorMap))
b""
phDiscard
(phCopyStateToState
(phRMStatusSlot 18)
(naturalAdd phDoorMap 40)
4
(phCheckStateZero32
b"doorbell-map"
(phTolerate mode)
(naturalAdd phDoorMap 40)
(phCall
phSysMmap
(phArgs
(phImm phDoorHost)
(phImm 0x10000)
(phImm 3)
(phImm phMapSharedFixed)
(phImm phFdCard)
(phImm 0))
b""
phDiscard
tail))))))))))
def phToken =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phTokP
(phZeros 4)
(phControl
b"control:phTok"
(phTolerate mode)
(phRMStatusSlot 15)
phTok
(phHClass (phABI abi 4))
0xc36f0108
phTokP
4
tail)))))
def phSchedule =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phSchedP
(phTake (phABI abi 9) (bytes 1 0 0))
(phControl
b"control:phSched"
(phTolerate mode)
(phRMStatusSlot 14)
phSched
phHGroup
0xa06c0101
phSchedP
(phABI abi 9)
tail)))))
def phVASpaceParams =
(lambda unrestricted uvm : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
(phZeros 48)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : Bytes .
(phSet64 (phSet64 (phSet32 (phZeros 48) 4 0x48) 8 0x1FFFFFB000000) 40 0x1000)))
uvm))
def phUVMLifecycle =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted lifecycle : (family NvidiaPlanHostLifecycle) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate
NvidiaPlanHostLifecycle
(lambda unrestricted current : (family NvidiaPlanHostLifecycle) .
(family NativePhysicalCommands))
lifecycle
(branch NvidiaPlanHostDirectRM entries . tail)
(branch NvidiaPlanHostUVM base extent . (phUVMPrepare mode base extent tail))))))
def phDMASelector =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phDMAObjectP
(phSet64 (phZeros 24) 8 0x1FFFFFFFFFFFF)
(phAlloc
b"alloc:phDMAObject"
(phTolerate mode)
phDMAObject
phHDevice
0x70
phDMAObjectP
24
phHDMA
(phRMStatusSlot 2)
tail))))
def phDirectActivate =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phFill
phBindP
(phW32 1)
(phControl
b"control:phBind"
(phTolerate mode)
(phRMStatusSlot 13)
phBind
(phHClass (phABI abi 4))
0xa06f0104
phBindP
4
(phSchedule abi mode (phToken abi mode (phDoorbell abi mode tail))))))))
def phUVMActivate =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phDoorbell
abi
mode
(phFill
phPreemptP
(phSet32 (phSet32 (phSet32 (phSet32 (phZeros 32) 0 1) 4 phHGroup) 8 0) 12 2)
(phControl
b"control:phPreempt"
(phTolerate mode)
(phRMStatusSlot 16)
phPreempt
phHSubdevice
0x20801210
phPreemptP
32
(phToken abi mode (phUVMRegisterChannelCommands abi mode (phSchedule abi mode tail)))))))))
-- 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 phChannelParams =
(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 phHError) 4 (phHMemory 0))
8
gpfifoGPU)
16
entries)
20
(naturalSelect direct (phABI abi 10) 0))
24
phHContext)
32
(naturalSelect direct (phHMemory 5) (phHMemory 0)))
64
(naturalSelect direct 0 nvidiaPlanHostUVMGPFIFOBytes))
128
(phABI abi 7))))))
-- ---- the driver's branch ----
-- NV_ESC_CHECK_VERSION_STR (0xD2, 72 bytes: cmd, reply, 64 version bytes)
-- with cmd '2', query: the driver writes its own version string. Its first
-- four bytes must be the branch the host's ABI was built for, or the host
-- stops, naming `driver-branch`, before any card call -- a 580-ABI host on a
-- 575 driver used to run until its DMA map failed (exit 120 at `dma-map`),
-- and on a 570 driver it faulted. Measured on the RTX 3090, 2026-09-24:
-- driver 580.178.04 answers `580.178.04`, reply 1. A driver that does not
-- answer leaves the bytes zero and is refused the same way.
def phCheckVersionIoctl : Nat =
0xC04846D2
def phVersion : Nat =
1024
def phRootAndDriverBranch =
(lambda unrestricted abi : (family NvidiaPlanHostABI) .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phAssertStateZero32
b"root"
offset
(phCopy
phVersion
(phSet32 (phZeros 72) 0 0x32)
(phCall
phSysIoctl
(phArgs3 (phSlot phSlotControl) (phImm phCheckVersionIoctl) (phState phVersion))
b""
phDiscard
(phCopy
phScratch
(phZeros 8)
(phCopyStateToState
phScratch
(naturalAdd phVersion 8)
4
(nativeLaunchRecipeAssertEqual
(phLoad phScratch)
(phImm (phABI abi 8))
b"driver-branch"
tail)))))))))
-- ---- the prelude: a working compute channel ----
-- 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 phDeviceSession =
(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
(phOpenSelectedCard
device
(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)
(phBindSelectedDevice
device
(phAlloc
b"alloc:phSub"
tolerate
phSub
phHDevice
0x2080
phSubP
4
phHSubdevice
(phRMStatusSlot 1)
(phExpectDeviceUUID
device
(phWhen
(naturalNonzero (bytes-length expectedName))
(phExpectName mode expectedName)
tail))))))))))))))))))))))
def phPreludeOn =
(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 =
(phHClass (phABI abi 4))
in
(let unrestricted tolerate =
(phTolerate mode)
in
(phDeviceSession
device
mode
abi
expectedName
(phWhen
uvm
(phDMASelector mode)
(phFill
phVASP
(phVASpaceParams uvm)
(phAlloc
b"alloc:phVAS"
tolerate
phVAS
phHDevice
0x90f1
phVASP
48
phHVASpace
(phRMStatusSlot 3)
(phUVMLifecycle
mode
lifecycle
(phBuffer
abi
mode
lifecycle
0
gpfifo
(phBuffer
abi
mode
lifecycle
1
push
(phBuffer
abi
mode
lifecycle
2
sem
(phBuffer
abi
mode
lifecycle
3
program
(phBuffer
abi
mode
lifecycle
4
qmd
(phWhen
direct
(phBuffer abi mode lifecycle 5 userd)
(phDataBuffers
abi
mode
lifecycle
6
data
(phFill
phErrP
(phMemoryParams 0 0 0 0 nvidiaPlanHostErrorPageBytes)
(phAlloc
b"alloc:phErr"
tolerate
phErr
phHDevice
0x3E
phErrP
128
phHError
(phRMStatusSlot 4)
(phWhen
(naturalNonzero errorHost)
(phMapMemory
b"error-map"
mode
phErrMap
phHError
0
nvidiaPlanHostErrorPageBytes
errorHost
(phRMStatusSlot 7))
(phFill
phGroupP
(phSet32
(phSet32 (phZeros 20) 8 (naturalSelect direct phHVASpace 0))
12
1)
(phAlloc
b"alloc:phGroup"
tolerate
phGroup
phHDevice
0xa06c
phGroupP
20
phHGroup
(phRMStatusSlot 5)
(phFill
phCtxP
(phSet32 (phSet32 (phZeros 12) 0 phHVASpace) 4 uvm)
(phAlloc
b"alloc:phCtx"
tolerate
phCtx
phHGroup
0x9067
phCtxP
12
phHContext
(phRMStatusSlot 6)
(phFill
phChanP
(phChannelParams abi direct (phRingEntries lifecycle) (phBufferGPU gpfifo))
(phAlloc
b"alloc:phChan"
tolerate
phChan
phHGroup
(phABI abi 4)
phChanP
368
channelClass
(phRMStatusSlot 8)
(phAlloc
b"alloc:phComp"
tolerate
phComp
channelClass
(phABI abi 5)
0
0
(phHClass (phABI abi 5))
(phRMStatusSlot 9)
(phAlloc
b"alloc:phUser"
tolerate
phUser
phHSubdevice
(phABI abi 6)
0
0
(phHClass (phABI abi 6))
(phRMStatusSlot 10)
(phWhen
direct
(phDirectActivate abi mode)
(phWhen uvm (phUVMActivate abi mode) tail)))))))))))))))))))))))))))))))))))
def phPrelude =
(phPreludeOn nvidiaDeviceZero)
-- ---- 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.
-- 20 us keeps the CPU cost negligible and the same ~600 s timeout
-- (polls x interval).
def nvidiaPlanHostFenceInterval : Nat =
20000
def nvidiaPlanHostFenceMaximumPolls : Nat =
30000000
def phUSERDHost =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate
NvidiaPlanHostLayout
(lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat)
layout
(branch
NvidiaPlanHostLayoutValue
gpfifo
push
sem
program
qmd
userd
data
abi
lifecycle
expectedName
errorHost
.
(phBufferHost userd))))
-- Release everything before exit: freeing the root client tears the whole
-- object hierarchy down synchronously. Left to the driver's asynchronous
-- reclaim at process exit, back-to-back hosts on the RTX 3090 hit
-- NV_ERR_INSUFFICIENT_RESOURCES on the channel allocation about a third of
-- the time, in streaks; v3 of this host, which did not free, did too.
def phRelease =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCopy
phFree
(phSet32 (phZeros 16) 12 phStatusSentinel)
(phCopyStateToState
phFree
(naturalAdd phRoot 8)
4
(phCopyStateToState
(naturalAdd phFree 4)
(naturalAdd phRoot 8)
4
(phCopyStateToState
(naturalAdd phFree 8)
(naturalAdd phRoot 8)
4
(phCall
phSysIoctl
(phArgs3 (phImm phFdControl) (phImm phRMFree) (phState phFree))
b""
phDiscard
(phCopyStateToState
(phRMStatusSlot 17)
(naturalAdd phFree 12)
4
(phAssertStateZero32 b"rm-free-root" (naturalAdd phFree 12) tail))))))))
-- The whole host, Strict: `submissions` is gpPut, the number of GPFIFO
-- entries the plan's tables carry; `fenceHost` the host address of the
-- semaphore slot the last submission releases; `statusHost`, when not 0, a
-- mapped address the UVM status record is copied to before the readbacks.
-- ---- native telemetry (docs/observability PRD item 9) ----
-- At each phase boundary the host appends an ALPHATEL record to
-- `alpha-host.alphatel` in its working directory: the body is
-- Runtime.NativeTelemetry's own encoding, made at build time (domain 1,
-- event 1 "reached", the boundary's ordinal as phase and sequence, status
-- 0, its name as payload), with the monotonic nanoseconds left zero; at
-- run time the host reads CLOCK_MONOTONIC and Runtime.NativeTelemetrySeal
-- writes the reading into the body, digests it and writes the record. A
-- record exists only if the host got there, so the last one names how far
-- a failed run came. The write is asserted whole (`telemetry-write`): a
-- host that cannot record says so and stops, rather than running unobserved.
-- Its pages: a fixed anonymous mapping of its own, taken before any device
-- call, so a host with no card still records its beginning.
def phTelemetryPage : Nat =
0x5E000000
def phTelemetryPadded : Nat =
0x5E000000
def phTelemetryRecord : Nat =
0x5E000400
def phTelemetryClock : Nat =
0x5E000800
def phTelemetryWork : Nat =
0x5E000C00
def phSlotTelemetry : Nat =
14
def phSlotTelemetryWritten : Nat =
15
def phTelemetryPath : Bytes =
b"alpha-host.alphatel\x00"
def phSysClockGettime : Nat =
228
def phClockMonotonic : Nat =
1
-- O_WRONLY | O_CREAT | O_APPEND, mode 0600
def phTelemetryOpenFlags : Nat =
1089
def phTelemetryMode : Nat =
384
def phTelemetryIdentity : Bytes =
(bytes-append
phIdentity
(phZeros (naturalSaturatingSubtract nativeTelemetryDigestBytes (bytes-length phIdentity))))
def phTelemetryZero : (family ModelWord64) =
(phWord 0)
-- the body Runtime.NativeTelemetry encodes for boundary `ordinal`, its
-- clock reading zero: no error code, the name as payload
def phTelemetryBody =
(lambda unrestricted ordinal : Nat .
(lambda unrestricted name : Bytes .
(nativeTelemetryRecordBody
(phWord ordinal)
phTelemetryZero
(byte 1)
(byte 1)
(nat-to-byte ordinal)
(byte 0)
(constructor
NativeTelemetryCounters
NativeTelemetryCountersValue
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero
phTelemetryZero)
phTelemetryIdentity
b""
name
phTelemetryZero
(phWord (bytes-length name)))))
-- the body with SHA-256's padding: 0x80, zeros to 56 mod 64, the bit length
-- (big-endian; a body is far below 8 KiB)
def phTelemetryPadding =
(lambda unrestricted length : Nat .
(bytes-cons
(byte 128)
(bytes-append
(phZeros (naturalModuloUnchecked (naturalSaturatingSubtract (naturalAdd 55 512) length) 64))
(bytes-append
(phZeros 6)
(bytes-cons
(nat-to-byte (naturalDivideUnchecked (naturalMultiply 8 length) 256))
(bytes-cons (nat-to-byte (naturalModuloUnchecked (naturalMultiply 8 length) 256)) b""))))))
-- map the telemetry page and put the magic in the record buffer
def phTelemetryOpen =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall
phSysMmap
(phArgs
(phImm phTelemetryPage)
(phImm 0x1000)
(phImm 3)
(phImm phMapAnonymousFixed)
(phImm phNoDescriptor)
(phImm 0))
b""
phDiscard
(phFill phTelemetryRecord b"ALPHATEL" tail)))
-- boundary `ordinal`, named: seal and append its record
def phTelemetry =
(lambda unrestricted ordinal : Nat .
(lambda unrestricted name : Bytes .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted body =
(phTelemetryBody ordinal name)
in
(let unrestricted length =
(bytes-length body)
in
(let unrestricted padded =
(bytes-append body (phTelemetryPadding length))
in
(phFill
phTelemetryPadded
padded
(phCall
phSysClockGettime
(phArgs3 (phImm phClockMonotonic) (phImm phTelemetryClock) (phImm 0))
b""
phDiscard
(phNext
(constructor
NativePhysicalOperation
NativePhysicalMachineRoutine
nativeTelemetrySealRoutine
(phArgs
(phImm phTelemetryPadded)
(phImm (naturalDivideUnchecked (bytes-length padded) 64))
(phImm phTelemetryRecord)
(phImm length)
(phImm phTelemetryClock)
(phImm phTelemetryWork))
phDiscard)
(phCall
phSysOpenat
(phArgs
(phImm phAtFdCwd)
phPayload
(phImm phTelemetryOpenFlags)
(phImm phTelemetryMode)
(phImm 0)
(phImm 0))
phTelemetryPath
(phStore phSlotTelemetry)
(phCall
phSysWrite
(phArgs3
(phSlot phSlotTelemetry)
(phImm phTelemetryRecord)
(phImm (naturalAdd 72 length)))
b""
(phStore phSlotTelemetryWritten)
(nativeLaunchRecipeAssertEqual
(phSlot phSlotTelemetryWritten)
(phImm (naturalAdd 72 length))
b"telemetry-write"
(phCall
phSysClose
(phArgs3 (phSlot phSlotTelemetry) (phImm 0) (phImm 0))
b""
phDiscard
tail)))))))))))))
-- Preparation has two ordered phases: envelope validation before any card
-- call, and expansion after the buffers exist. Keeping these continuations
-- here gives recipe-backed probes the same telemetry and submit/wait path
-- as the ordinary host, without copying its RM command stream.
def nvidiaPlanHostPreparedCommandsOn =
(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
(phPreludeOn
device
(constructor NvidiaPlanHostMode NvidiaPlanHostStrict)
layout
(phTelemetry
1
b"plan-host:channel-ready"
(mapped
(phFills
fills
(phTelemetry
2
b"plan-host:uploaded"
(phLoadToken
(phPublish
(naturalAdd
(phUSERDHost layout)
nvidiaPlanHostUSERDGPPutOffset)
submissions
(phTelemetry
3
b"plan-host:submitted"
(phNext
(constructor
NativePhysicalOperation
NativePhysicalFenceWait
(phImm fenceHost)
(phImm nvidiaPlanHostFenceValue)
(phWord nvidiaPlanHostFenceMaximumPolls)
(phWord nvidiaPlanHostFenceInterval))
(phTelemetry
4
b"plan-host:completed"
(phWhen
(naturalNonzero statusHost)
(phCopyStateToMapped
phUVMStatusRecord
statusHost
phUVMStatusRecordExtent)
(phReads
reads
(phTelemetry
5
b"plan-host:read-back"
(phCall
phSysExitGroup
(phArgs3 (phImm 0) (phImm 0) (phImm 0))
b""
phDiscard
(phNext
(constructor
NativePhysicalOperation
NativePhysicalHaltSuccess)
(constructor
NativePhysicalCommands
NativePhysicalCommandsEnd)))))))))))))))))))))))))))))
def nvidiaPlanHostPreparedCommands =
(nvidiaPlanHostPreparedCommandsOn nvidiaDeviceZero)
def phNoPreparation =
(lambda unrestricted tail : (family NativePhysicalCommands) . tail)
def nvidiaPlanHostCommandsOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(nvidiaPlanHostPreparedCommandsOn device phNoPreparation phNoPreparation))
def nvidiaPlanHostCommands =
(nvidiaPlanHostCommandsOn nvidiaDeviceZero)
-- 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 nvidiaPlanHostProbeCommandsOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(phPipeCreate
(phPreludeOn
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 nvidiaPlanHostProbeCommands =
(nvidiaPlanHostProbeCommandsOn nvidiaDeviceZero)
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 nvidiaPlanHostPreludeCommands =
(lambda unrestricted mode : (family NvidiaPlanHostMode) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(phPrelude mode layout (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
def nvidiaPlanHostProgram =
(lambda unrestricted identity : Bytes .
(lambda unrestricted commands : (family NativePhysicalCommands) .
(constructor
NativePhysicalProgram
NativePhysicalProgramValue
(phWord phStateExtent)
(phWord phSlots)
commands
(phCommandCount commands)
identity
zero)))
def nvidiaPlanHostELF =
(lambda unrestricted identity : Bytes .
(lambda unrestricted commands : (family NativePhysicalCommands) .
(nativePhysicalGenerateNativeELFBytesDirect (nvidiaPlanHostProgram identity commands))))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.