module Coppelius.Build.RTX3090

import Accelerator.SM86.Capability
import Coppelius.Build.SM86Compat
import Coppelius.Learner
import Coppelius.SM86Capability
import Coppelius.TrainingRun
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 Coppelius.Build.NativeHost
import Platform.Linux.Nvidia.Compatibility

-- R6 keeps the conservative qualified SM86 schedule.  This binding changes
-- target identity and exact product guard, not model geometry or tuning.
family CoppeliusRTX3090Binding : Type 0
constructor CoppeliusRTX3090BindingValue
field unrestricted coppeliusRTX3090SemanticBinding : (family CoppeliusSM86BuildBinding)
field unrestricted coppeliusRTX3090TargetProfile : (family RunPodSM86TargetProfile)
field unrestricted coppeliusRTX3090ObservedCapabilities : (family SM86DeviceCapabilities)
field unrestricted coppeliusRTX3090Admission : (family SM86CapabilityAdmission)
field unrestricted coppeliusRTX3090Plan : (family SystemTargetBuildPlan)

end-family

def coppeliusRTX3090TargetIdentity : Bytes =
  runPodRTX3090TargetIdentity

def coppeliusRTX3090QualificationIdentity : Bytes =
  b"coppelius-rtx3090-target-profile-v1"

def coppeliusRTX3090TotalVideoMemory : StdU64 =
  (runPodSM86TotalVideoMemory runPodRTX3090TargetProfile)

def coppeliusRTX3090Capabilities : (family SM86DeviceCapabilities) =
  (record
    SM86DeviceCapabilities
    (sm86CapabilityComputeMajor = 8)
    (sm86CapabilityComputeMinor = 6)
    (sm86CapabilityTotalVideoMemoryBytes = coppeliusRTX3090TotalVideoMemory)
    (sm86CapabilityAvailableVideoMemoryBytes
      =
      (stdByteCountValue coppeliusSM86CompatMinimumVideoMemory))
    (sm86CapabilityMappedAddressEnd = (stdDeviceAddressValue coppeliusSM86CompatMappedAddressEnd))
    (sm86CapabilityMaximumGridX
      =
      (stdU32ToNatural (stdGridDimensionValue coppeliusSM86CompatMaximumGridX)))
    (sm86CapabilityUVMSupported = 1)
    (sm86CapabilityResourceManagerSupported = 1)
    (sm86CapabilityQMDSupported = 1)
    (sm86CapabilityPushbufferSupported = 1)
    (sm86CapabilityGPFIFOSupported = 1)
    (sm86CapabilityDeviceTimestampsSupported = 1)
    (sm86CapabilityHostFallbacks = 0))

def coppeliusRTX3090CapabilityAdmission : (family SM86CapabilityAdmission) =
  (coppeliusSM86CompatAdmit coppeliusRTX3090Capabilities)

def coppeliusRTX3090CapabilityAccepted : Nat =
  (sm86CapabilityAdmissionAccepted coppeliusRTX3090CapabilityAdmission)

-- 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 coppeliusRTX3090CompatibilityRefusal : Bytes =
  (nvidiaCompatibilityRefusal (coppeliusCompatDemands runPodSM86QMDArchitecture) runPodRTX3090Supplies)

def coppeliusRTX3090ExactTargetAccepted : Nat =
  (naturalAnd (naturalIsZero (bytes-length coppeliusRTX3090CompatibilityRefusal))
  (naturalAnd
    (runPodSM86TargetMatches
      runPodRTX3090TargetProfile
      runPodRTX3090ProductIdentity
      coppeliusRTX3090Capabilities)
    coppeliusRTX3090CapabilityAccepted))

def coppeliusRTX3090BuildPlanEntries =
  (coppeliusSM86BuildPlanEntries
    coppeliusRTX3090TargetIdentity
    coppeliusRTX3090QualificationIdentity
    b"coppelius-rtx3090-sm86.elf"
    b"systems/coppelius/evidence/rtx3090-sm86-compat-20260917/README.md"
    b"r6-qualification-pending")

def coppeliusRTX3090BuildPlan : (family SystemTargetBuildPlan) =
  (record
    SystemTargetBuildPlan
    (systemTargetBuildPlanIdentity = b"coppelius-rtx3090-build-plan-v1")
    (systemTargetBuildPlanCapabilityAccepted = coppeliusRTX3090ExactTargetAccepted)
    (systemTargetBuildPlanEntries = coppeliusRTX3090BuildPlanEntries))

def coppeliusRTX3090BuildRequest : (family SystemTargetBuildRequest) =
  (record
    SystemTargetBuildRequest
    (buildRequestSystemIdentity = b"coppelius")
    (buildRequestLearnerIdentity = coppeliusLearnerIdentity)
    (buildRequestTargetIdentity = coppeliusRTX3090TargetIdentity)
    (buildRequestAdmissionAccepted = coppeliusRTX3090ExactTargetAccepted)
    (buildRequestScheduleIdentity = b"sm86-qmd-pushbuffer-gpfifo-v1")
    (buildRequestMemoryIdentity = b"coppelius-sm86-static-arena-1280-mib")
    (buildRequestProtocolIdentity = b"alpha-text-artifact-request-v1")
    (buildRequestCheckpointIdentity = coppeliusRawCheckpointSchemaIdentity)
    (buildRequestOutputFilename = b"coppelius-rtx3090-sm86.elf")
    (buildRequestArtifactRoot = b"systems/coppelius/src/Coppelius/Build/RTX3090Artifact.alpha")
    (buildRequestArtifactExpression = b"artifact"))

def coppeliusRTX3090Binding : (family CoppeliusRTX3090Binding) =
  (record
    CoppeliusRTX3090Binding
    (coppeliusRTX3090SemanticBinding = coppeliusSM86BuildBinding)
    (coppeliusRTX3090TargetProfile = runPodRTX3090TargetProfile)
    (coppeliusRTX3090ObservedCapabilities = coppeliusRTX3090Capabilities)
    (coppeliusRTX3090Admission = coppeliusRTX3090CapabilityAdmission)
    (coppeliusRTX3090Plan = coppeliusRTX3090BuildPlan))