module Platform.RunPod.Nvidia.SM86 import Accelerator.SM86.Capability import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Platform.Linux.Nvidia.Compatibility import Platform.Linux.Nvidia.Memory.ABI import Std.List import Std.Natural import Std.Word -- A concrete target profile is stricter than generic SM86 capability -- admission. It binds an artifact to one exact provider-visible product while -- leaving model and learner packages unaware of any card name. family RunPodSM86TargetProfile : Type 0 constructor RunPodSM86TargetProfileValue field unrestricted runPodSM86TargetIdentityValue : Bytes field unrestricted runPodSM86ProductIdentityValue : Bytes field unrestricted runPodSM86ComputeMajorValue : Nat field unrestricted runPodSM86ComputeMinorValue : Nat field unrestricted runPodSM86TotalVideoMemoryValue : (family ModelWord64) end-family def runPodRTX3070TargetIdentity : Bytes = b"runpod-nvidia-geforce-rtx3070-sm86" def runPodRTX3070ProductIdentity : Bytes = b"NVIDIA GeForce RTX 3070" def runPodRTX3070TotalVideoMemory : StdU64 = 0x0000_0002_0000_0000 def runPodRTX3070TargetProfile : (family RunPodSM86TargetProfile) = (record RunPodSM86TargetProfile (runPodSM86TargetIdentityValue = runPodRTX3070TargetIdentity) (runPodSM86ProductIdentityValue = runPodRTX3070ProductIdentity) (runPodSM86ComputeMajorValue = 8) (runPodSM86ComputeMinorValue = 6) (runPodSM86TotalVideoMemoryValue = runPodRTX3070TotalVideoMemory)) def runPodRTX3090TargetIdentity : Bytes = b"runpod-nvidia-geforce-rtx3090-sm86" def runPodRTX3090ProductIdentity : Bytes = b"NVIDIA GeForce RTX 3090" def runPodRTX3090TotalVideoMemory : StdU64 = 0x0000_0006_0000_0000 def runPodRTX3090TargetProfile : (family RunPodSM86TargetProfile) = (record RunPodSM86TargetProfile (runPodSM86TargetIdentityValue = runPodRTX3090TargetIdentity) (runPodSM86ProductIdentityValue = runPodRTX3090ProductIdentity) (runPodSM86ComputeMajorValue = 8) (runPodSM86ComputeMinorValue = 6) (runPodSM86TotalVideoMemoryValue = runPodRTX3090TotalVideoMemory)) -- Ampere command-stream facts belong to the exact target package. Systems -- consume these values when late realization derives QMDs and pushbuffers; -- they never branch on a card name or copy driver constants. def runPodSM86QMDArchitecture : (family ModelWord32) = (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0)) -- Ampere QMD v0.3 occupies one 256-byte SEND_PCAS slot. This is a target -- command-format fact, separate from the number of launches a system emits. def runPodSM86QMDSlotBytes : Nat = 256 def runPodSM86ComputeClass : (family ModelWord32) = (constructor ModelWord32 ModelWord32Value (byte 192) (byte 199) (byte 0) (byte 0)) def runPodSM86SPAVersion : (family ModelWord32) = (constructor ModelWord32 ModelWord32Value (byte 6) (byte 8) (byte 0) (byte 0)) def runPodSM86TargetIdentity = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes) profile (branch RunPodSM86TargetProfileValue targetIdentity productIdentity computeMajor computeMinor totalVideoMemory . targetIdentity))) def runPodSM86TotalVideoMemory = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family ModelWord64)) profile (branch RunPodSM86TargetProfileValue targetIdentity productIdentity computeMajor computeMinor totalVideoMemory . totalVideoMemory))) def runPodSM86ProductIdentity = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . Bytes) profile (branch RunPodSM86TargetProfileValue targetIdentity productIdentity computeMajor computeMinor totalVideoMemory . productIdentity))) -- NV2080_CTRL_CMD_GPU_GET_NAME_STRING uses one fixed 64-byte ASCII field. -- The concrete product identity remains readable source text and only the ABI -- projection adds its required trailing NUL bytes. def runPodSM86ProductIdentityPadded = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (bytes-append (runPodSM86ProductIdentity profile) (memoryABIZeroBytes (naturalSaturatingSubtract 64 (bytes-length (runPodSM86ProductIdentity profile)))))) -- Product matching is a pre-submission guard. The system-specific generic -- SM86 admission remains a second, independent check for memory, addresses, -- grid, RM/UVM, command formats, timestamps and absence of fallback. def runPodSM86TargetMatches = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (lambda unrestricted observedProductIdentity : Bytes . (lambda unrestricted observed : (family SM86DeviceCapabilities) . (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . Nat) profile (branch RunPodSM86TargetProfileValue targetIdentity requiredProductIdentity requiredMajor requiredMinor requiredTotalVideoMemory . (eliminate SM86DeviceCapabilities (lambda unrestricted current : (family SM86DeviceCapabilities) . Nat) observed (branch SM86DeviceCapabilitiesValue observedMajor observedMinor observedTotalVideoMemory observedAvailableVideoMemory observedMappedAddressEnd observedMaximumGridX observedUVM observedResourceManager observedQMD observedPushbuffer observedGPFIFO observedTimestamps observedFallbacks . (naturalAnd (bytes-equal observedProductIdentity requiredProductIdentity) (naturalAnd (naturalEqual observedMajor requiredMajor) (naturalAnd (naturalEqual observedMinor requiredMinor) (modelWord64Equal observedTotalVideoMemory requiredTotalVideoMemory))))))))))) -- ---- what the cards supply (Platform.Linux.Nvidia.Compatibility) ---- -- The architecture's, with its source; the rest as the qualified runs on -- the card recorded them (`record`: the run's evidence). def runPodSM86Architectural = (lambda unrestricted source : Bytes . (constructor NvidiaEvidence NvidiaEvidenceArchitectural source)) def runPodSM86Supplies = (lambda unrestricted profile : (family RunPodSM86TargetProfile) . (lambda unrestricted record : Bytes . (let unrestricted measured = (constructor NvidiaEvidence NvidiaEvidenceMeasured record) in (eliminate RunPodSM86TargetProfile (lambda unrestricted current : (family RunPodSM86TargetProfile) . (family StdList (family NvidiaSupply))) profile (branch RunPodSM86TargetProfileValue target product major minor memory . (nvidiaSupply b"instruction-set" (naturalAdd (naturalMultiply 10 major) minor) (runPodSM86Architectural b"NVIDIA Ampere GA10x: compute capability 8.6 (CUDA C++ Programming Guide, compute capabilities)") (nvidiaSupply b"compute-class" (modelWord32ToNatural runPodSM86ComputeClass) (runPodSM86Architectural b"AMPERE_COMPUTE_B (open-gpu-kernel-modules, clc7c0.h)") (nvidiaSupply b"registers-per-thread" 255 (runPodSM86Architectural b"SM86: an 8-bit register operand, R255 the zero register (Accelerator.SM86.Types)") (nvidiaSupply b"threads-per-block" 1024 (runPodSM86Architectural b"compute capability 8.6: at most 1024 threads per block") (nvidiaSupply b"shared-bytes-per-block" 49152 (runPodSM86Architectural b"compute capability 8.6: 48 KiB of static shared memory per block") (nvidiaSupply b"driver-branch" (nvidiaCompatibilityTextWord b"580.") measured (nvidiaSupply b"unified-memory" 1 measured (nvidiaSupply b"video-memory-bytes" (modelWord64Natural memory) measured nvidiaNoSupplies))))))))))))) def runPodRTX3070Record : Bytes = b"tests/observability/import/envelope-rtx3070/README.md" def runPodRTX3090Record : Bytes = b"tests/observability/import/bob-rtx3090/README.md" def runPodRTX3070Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3070TargetProfile runPodRTX3070Record) def runPodRTX3090Supplies : (family StdList (family NvidiaSupply)) = (runPodSM86Supplies runPodRTX3090TargetProfile runPodRTX3090Record)