module Bob.Build.RTX3090

import Accelerator.SM86.Capability
import Bob.Build.SM86
import Model.Parameter
import Model.Word64
import Platform.RunPod.Nvidia.SM86
import Representation.BuildRequest
import Representation.BuildPlan
import Std.Natural
import Std.Physical
import Std.Word
import Bob.Build.NativeHost
import Platform.Linux.Nvidia.Compatibility

def bobRTX3090TargetIdentity : Bytes =
  runPodRTX3090TargetIdentity

def bobRTX3090QualificationIdentity : Bytes =
  b"bob-rtx3090-target-profile-v1"

def bobRTX3090Capabilities : (family SM86DeviceCapabilities) =
  (record
    SM86DeviceCapabilities
    (sm86CapabilityComputeMajor = 8)
    (sm86CapabilityComputeMinor = 6)
    (sm86CapabilityTotalVideoMemoryBytes = (runPodSM86TotalVideoMemory runPodRTX3090TargetProfile))
    (sm86CapabilityAvailableVideoMemoryBytes = (stdByteCountValue bobSM86MinimumVideoMemory))
    (sm86CapabilityMappedAddressEnd = (stdDeviceAddressValue bobSM86MappedAddressEnd))
    (sm86CapabilityMaximumGridX = (stdU32ToNatural (stdGridDimensionValue bobSM86MaximumGridX)))
    (sm86CapabilityUVMSupported = 1)
    (sm86CapabilityResourceManagerSupported = 1)
    (sm86CapabilityQMDSupported = 1)
    (sm86CapabilityPushbufferSupported = 1)
    (sm86CapabilityGPFIFOSupported = 1)
    (sm86CapabilityDeviceTimestampsSupported = 1)
    (sm86CapabilityHostFallbacks = 0))

def bobRTX3090CapabilityAccepted : Nat =
  (sm86CapabilityAdmissionAccepted (bobSM86Admit bobRTX3090Capabilities))

-- the compatibility contract: what the artifact demands of the card
-- against what the RTX 3090 profile supplies (Platform.Linux.Nvidia.
-- Compatibility); the first demand not met, by name (empty = admitted)
def bobRTX3090CompatibilityRefusal : Bytes =
  (nvidiaCompatibilityRefusal (bobCompatDemands runPodSM86QMDArchitecture) runPodRTX3090Supplies)

def bobRTX3090ExactTargetAccepted : Nat =
  (naturalAnd (naturalIsZero (bytes-length bobRTX3090CompatibilityRefusal))
  (naturalAnd
    (runPodSM86TargetMatches
      runPodRTX3090TargetProfile
      runPodRTX3090ProductIdentity
      bobRTX3090Capabilities)
    bobRTX3090CapabilityAccepted))

def bobRTX3090BuildPlan : (family SystemTargetBuildPlan) =
  (record
    SystemTargetBuildPlan
    (systemTargetBuildPlanIdentity = b"bob-rtx3090-build-plan-v1")
    (systemTargetBuildPlanCapabilityAccepted = bobRTX3090ExactTargetAccepted)
    (systemTargetBuildPlanEntries
      =
      (bobSM86BuildPlanEntries
        bobRTX3090TargetIdentity
        bobRTX3090QualificationIdentity
        b"bob-rtx3090-sm86.elf")))

def bobRTX3090BuildRequest : (family SystemTargetBuildRequest) =
  (record
    SystemTargetBuildRequest
    (buildRequestSystemIdentity = b"bob")
    (buildRequestLearnerIdentity = b"adamw")
    (buildRequestTargetIdentity = bobRTX3090TargetIdentity)
    (buildRequestAdmissionAccepted = bobRTX3090ExactTargetAccepted)
    (buildRequestScheduleIdentity = b"row-gather-ece256-adamw-greedy")
    (buildRequestMemoryIdentity = b"bob-sm86-static-arena-16-mib")
    (buildRequestProtocolIdentity = b"alpha-text-artifact-request-v1")
    (buildRequestCheckpointIdentity = b"bob-raw-pmv-f32-v1")
    (buildRequestOutputFilename = b"bob-rtx3090-sm86.elf")
    (buildRequestArtifactRoot = b"systems/bob/src/Bob/Build/RTX3090Artifact.alpha")
    (buildRequestArtifactExpression = b"artifact"))