Platform.RunPod.Nvidia.SM86

1module Platform.RunPod.Nvidia.SM86
2
3import Accelerator.SM86.Capability
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Platform.Linux.Nvidia.Compatibility
9import Platform.Linux.Nvidia.Memory.ABI
10import Std.List
11import Std.Natural
12import Std.Word
13
14-- A concrete target profile is stricter than generic SM86 capability
15-- admission.  It binds an artifact to one exact provider-visible product while
16-- leaving model and learner packages unaware of any card name.
17family RunPodSM86TargetProfile : Type 0
18constructor RunPodSM86TargetProfileValue
19field unrestricted runPodSM86TargetIdentityValue : Bytes
20field unrestricted runPodSM86ProductIdentityValue : Bytes
21field unrestricted runPodSM86ComputeMajorValue : Nat
22field unrestricted runPodSM86ComputeMinorValue : Nat
23field unrestricted runPodSM86TotalVideoMemoryValue : (family ModelWord64)
24-- what the driver keeps of it before any process allocates (nvidia-smi -q
25-- -d MEMORY, "Reserved"): a process can allocate total - reserved at most
26field unrestricted runPodSM86ReservedVideoMemoryValue : (family ModelWord64)
27
28end-family
29
30def runPodRTX3070TargetIdentity : Bytes =
31  b"runpod-nvidia-geforce-rtx3070-sm86"
32
33def runPodRTX3070ProductIdentity : Bytes =
34  b"NVIDIA GeForce RTX 3070"
35
36def runPodRTX3070TotalVideoMemory : StdU64 =
37  0x0000_0002_0000_0000
38
39-- 352 MiB, measured on a RunPod RTX 3070, driver 580.126.20, 2026-10-04
40def runPodRTX3070ReservedVideoMemory : StdU64 =
41  0x0000_0000_1600_0000
42
43def runPodRTX3070TargetProfile : (family RunPodSM86TargetProfile) =
44  (record
45    RunPodSM86TargetProfile
46    (runPodSM86TargetIdentityValue = runPodRTX3070TargetIdentity)
47    (runPodSM86ProductIdentityValue = runPodRTX3070ProductIdentity)
48    (runPodSM86ComputeMajorValue = 8)
49    (runPodSM86ComputeMinorValue = 6)
50    (runPodSM86TotalVideoMemoryValue = runPodRTX3070TotalVideoMemory)
51    (runPodSM86ReservedVideoMemoryValue = runPodRTX3070ReservedVideoMemory))
52
53def runPodRTX3090TargetIdentity : Bytes =
54  b"runpod-nvidia-geforce-rtx3090-sm86"
55
56def runPodRTX3090ProductIdentity : Bytes =
57  b"NVIDIA GeForce RTX 3090"
58
59def runPodRTX3090TotalVideoMemory : StdU64 =
60  0x0000_0006_0000_0000
61
62-- 452 MiB, measured on the RunPod RTX 3090, driver 580.126.20, 2026-10-04
63def runPodRTX3090ReservedVideoMemory : StdU64 =
64  0x0000_0000_1C40_0000
65
66def runPodRTX3090TargetProfile : (family RunPodSM86TargetProfile) =
67  (record
68    RunPodSM86TargetProfile
69    (runPodSM86TargetIdentityValue = runPodRTX3090TargetIdentity)
70    (runPodSM86ProductIdentityValue = runPodRTX3090ProductIdentity)
71    (runPodSM86ComputeMajorValue = 8)
72    (runPodSM86ComputeMinorValue = 6)
73    (runPodSM86TotalVideoMemoryValue = runPodRTX3090TotalVideoMemory)
74    (runPodSM86ReservedVideoMemoryValue = runPodRTX3090ReservedVideoMemory))
75
76-- Ampere command-stream facts belong to the exact target package.  Systems
77-- consume these values when late realization derives QMDs and pushbuffers;
78-- they never branch on a card name or copy driver constants.
79def runPodSM86QMDArchitecture : (family ModelWord32) =
80  (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
81
82-- Ampere QMD v0.3 occupies one 256-byte SEND_PCAS slot. This is a target
83-- command-format fact, separate from the number of launches a system emits.
84def runPodSM86QMDSlotBytes : Nat = 256
85
86def runPodSM86ComputeClass : (family ModelWord32) =
87  (constructor ModelWord32 ModelWord32Value (byte 192) (byte 199) (byte 0) (byte 0))
88
89def runPodSM86SPAVersion : (family ModelWord32) =
90  (constructor ModelWord32 ModelWord32Value (byte 6) (byte 8) (byte 0) (byte 0))
91
92def runPodSM86TargetIdentity =
93  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
94    (eliminate
95      RunPodSM86TargetProfile
96      (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes)
97      profile
98      (branch
99        RunPodSM86TargetProfileValue
100        targetIdentity
101        productIdentity
102        computeMajor
103        computeMinor
104        totalVideoMemory
105        reservedVideoMemory
106        .
107        targetIdentity)))
108
109def runPodSM86TotalVideoMemory =
110  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
111    (eliminate
112      RunPodSM86TargetProfile
113      (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family ModelWord64))
114      profile
115      (branch
116        RunPodSM86TargetProfileValue
117        targetIdentity
118        productIdentity
119        computeMajor
120        computeMinor
121        totalVideoMemory
122        reservedVideoMemory
123        .
124        totalVideoMemory)))
125
126def runPodSM86ReservedVideoMemory =
127  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
128    (eliminate
129      RunPodSM86TargetProfile
130      (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family ModelWord64))
131      profile
132      (branch
133        RunPodSM86TargetProfileValue
134        targetIdentity
135        productIdentity
136        computeMajor
137        computeMinor
138        totalVideoMemory
139        reservedVideoMemory
140        .
141        reservedVideoMemory)))
142
143-- what one process can allocate: total less the driver's reservation
144def runPodSM86UsableVideoMemory =
145  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
146    (naturalSaturatingSubtract
147      (modelWord64Natural (runPodSM86TotalVideoMemory profile))
148      (modelWord64Natural (runPodSM86ReservedVideoMemory profile))))
149
150def runPodSM86ProductIdentity =
151  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
152    (eliminate
153      RunPodSM86TargetProfile
154      (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes)
155      profile
156      (branch
157        RunPodSM86TargetProfileValue
158        targetIdentity
159        productIdentity
160        computeMajor
161        computeMinor
162        totalVideoMemory
163        reservedVideoMemory
164        .
165        productIdentity)))
166
167-- NV2080_CTRL_CMD_GPU_GET_NAME_STRING uses one fixed 64-byte ASCII field.
168-- The concrete product identity remains readable source text and only the ABI
169-- projection adds its required trailing NUL bytes.
170def runPodSM86ProductIdentityPadded =
171  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
172    (bytes-append
173      (runPodSM86ProductIdentity profile)
174      (memoryABIZeroBytes
175        (naturalSaturatingSubtract 64 (bytes-length (runPodSM86ProductIdentity profile))))))
176
177-- Product matching is a pre-submission guard.  The system-specific generic
178-- SM86 admission remains a second, independent check for memory, addresses,
179-- grid, RM/UVM, command formats, timestamps and absence of fallback.
180def runPodSM86TargetMatches =
181  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
182    (lambda unrestricted observedProductIdentity : Bytes .
183      (lambda unrestricted observed : (family SM86DeviceCapabilities) .
184        (eliminate
185          RunPodSM86TargetProfile
186          (lambda unrestricted current : (family RunPodSM86TargetProfile) . Nat)
187          profile
188          (branch
189            RunPodSM86TargetProfileValue
190            targetIdentity
191            requiredProductIdentity
192            requiredMajor
193            requiredMinor
194            requiredTotalVideoMemory
195            requiredReservedVideoMemory
196            .
197            (eliminate
198              SM86DeviceCapabilities
199              (lambda unrestricted current : (family SM86DeviceCapabilities) . Nat)
200              observed
201              (branch
202                SM86DeviceCapabilitiesValue
203                observedMajor
204                observedMinor
205                observedTotalVideoMemory
206                observedAvailableVideoMemory
207                observedMappedAddressEnd
208                observedMaximumGridX
209                observedUVM
210                observedResourceManager
211                observedQMD
212                observedPushbuffer
213                observedGPFIFO
214                observedTimestamps
215                observedFallbacks
216                .
217                (naturalAnd
218                  (bytes-equal observedProductIdentity requiredProductIdentity)
219                  (naturalAnd
220                    (naturalEqual observedMajor requiredMajor)
221                    (naturalAnd
222                      (naturalEqual observedMinor requiredMinor)
223                      (modelWord64Equal observedTotalVideoMemory requiredTotalVideoMemory)))))))))))
224
225-- ---- what the cards supply (Platform.Linux.Nvidia.Compatibility) ----
226-- The architecture's, with its source; the rest as the qualified runs on
227-- the card recorded them (`record`: the run's evidence).
228def runPodSM86Architectural = (lambda unrestricted source : Bytes . (constructor NvidiaEvidence NvidiaEvidenceArchitectural source))
229
230def runPodSM86Supplies =
231  (lambda unrestricted profile : (family RunPodSM86TargetProfile) .
232    (lambda unrestricted record : Bytes .
233      (let unrestricted measured = (constructor NvidiaEvidence NvidiaEvidenceMeasured record) in
234      (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family StdList (family NvidiaSupply))) profile
235        (branch RunPodSM86TargetProfileValue target product major minor memory reserved .
236          (nvidiaSupply b"instruction-set" (naturalAdd (naturalMultiply 10 major) minor)
237            (runPodSM86Architectural b"NVIDIA Ampere GA10x: compute capability 8.6 (CUDA C++ Programming Guide, compute capabilities)")
238          (nvidiaSupply b"compute-class" (modelWord32ToNatural runPodSM86ComputeClass)
239            (runPodSM86Architectural b"AMPERE_COMPUTE_B (open-gpu-kernel-modules, clc7c0.h)")
240          (nvidiaSupply b"registers-per-thread" 255
241            (runPodSM86Architectural b"SM86: an 8-bit register operand, R255 the zero register (Accelerator.SM86.Types)")
242          (nvidiaSupply b"threads-per-block" 1024
243            (runPodSM86Architectural b"compute capability 8.6: at most 1024 threads per block")
244          (nvidiaSupply b"shared-bytes-per-block" 49152
245            (runPodSM86Architectural b"compute capability 8.6: 48 KiB of static shared memory per block")
246          (nvidiaSupply b"driver-branch" (nvidiaCompatibilityTextWord b"580.") measured
247          (nvidiaSupply b"unified-memory" 1 measured
248          (nvidiaSupply b"video-memory-bytes" (modelWord64Natural memory) measured
249            nvidiaNoSupplies)))))))))))))
250
251def runPodRTX3070Record : Bytes = b"tests/observability/import/envelope-rtx3070/README.md"
252def runPodRTX3090Record : Bytes = b"tests/observability/import/bob-rtx3090/README.md"
253
254def runPodRTX3070Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3070TargetProfile runPodRTX3070Record)
255def runPodRTX3090Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3090TargetProfile runPodRTX3090Record)