module Coppelius.Build.RTX3070

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

-- R5's one physical target.  The exact self-contained ELF completed fresh
-- initialization and fresh-process continuation on this device on 2026-09-17.
-- Marketing identity remains evidence; capability admission stays generic.
family CoppeliusRTX3070Binding : Type 0
constructor CoppeliusRTX3070BindingValue
field unrestricted coppeliusRTX3070SemanticBinding : (family CoppeliusSM86BuildBinding)
field unrestricted coppeliusRTX3070TargetProfile : (family RunPodSM86TargetProfile)
field unrestricted coppeliusRTX3070ObservedCapabilities : (family SM86DeviceCapabilities)
field unrestricted coppeliusRTX3070Admission : (family SM86CapabilityAdmission)
field unrestricted coppeliusRTX3070Plan : (family SystemTargetBuildPlan)

end-family

def coppeliusRTX3070TargetIdentity : Bytes =
  runPodRTX3070TargetIdentity

def coppeliusRTX3070QualificationIdentity : Bytes =
  b"coppelius-rtx3070-target-profile-v1"

def coppeliusRTX3070TotalVideoMemory : StdU64 =
  (runPodSM86TotalVideoMemory runPodRTX3070TargetProfile)

def coppeliusRTX3070Capabilities : (family SM86DeviceCapabilities) =
  (record
    SM86DeviceCapabilities
    (sm86CapabilityComputeMajor = 8)
    (sm86CapabilityComputeMinor = 6)
    (sm86CapabilityTotalVideoMemoryBytes = coppeliusRTX3070TotalVideoMemory)
    (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 coppeliusRTX3070CapabilityAdmission : (family SM86CapabilityAdmission) =
  (coppeliusSM86CompatAdmit coppeliusRTX3070Capabilities)

def coppeliusRTX3070CapabilityAccepted : Nat =
  (sm86CapabilityAdmissionAccepted coppeliusRTX3070CapabilityAdmission)

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

def coppeliusRTX3070ExactTargetAccepted : Nat =
  (naturalAnd (naturalIsZero (bytes-length coppeliusRTX3070CompatibilityRefusal))
  (naturalAnd
    (runPodSM86TargetMatches
      runPodRTX3070TargetProfile
      runPodRTX3070ProductIdentity
      coppeliusRTX3070Capabilities)
    coppeliusRTX3070CapabilityAccepted))

def coppeliusRTX3070BuildPlanEntries =
  (coppeliusSM86BuildPlanEntries
    coppeliusRTX3070TargetIdentity
    coppeliusRTX3070QualificationIdentity
    b"coppelius-rtx3070-sm86.elf"
    b"systems/coppelius/evidence/2026-09-17-alpha-owned-self-contained-training-elf.md"
    b"r6-qualification-pending")

def coppeliusRTX3070BuildPlan : (family SystemTargetBuildPlan) =
  (record
    SystemTargetBuildPlan
    (systemTargetBuildPlanIdentity = b"coppelius-rtx3070-build-plan-v1")
    (systemTargetBuildPlanCapabilityAccepted = coppeliusRTX3070ExactTargetAccepted)
    (systemTargetBuildPlanEntries = coppeliusRTX3070BuildPlanEntries))

def coppeliusRTX3070BuildRequest : (family SystemTargetBuildRequest) =
  (record
    SystemTargetBuildRequest
    (buildRequestSystemIdentity = b"coppelius")
    (buildRequestLearnerIdentity = coppeliusLearnerIdentity)
    (buildRequestTargetIdentity = coppeliusRTX3070TargetIdentity)
    (buildRequestAdmissionAccepted = coppeliusRTX3070ExactTargetAccepted)
    (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-rtx3070-sm86.elf")
    (buildRequestArtifactRoot = b"systems/coppelius/src/Coppelius/Build/RTX3070Artifact.alpha")
    (buildRequestArtifactExpression = b"artifact"))

def coppeliusRTX3070Binding : (family CoppeliusRTX3070Binding) =
  (record
    CoppeliusRTX3070Binding
    (coppeliusRTX3070SemanticBinding = coppeliusSM86BuildBinding)
    (coppeliusRTX3070TargetProfile = runPodRTX3070TargetProfile)
    (coppeliusRTX3070ObservedCapabilities = coppeliusRTX3070Capabilities)
    (coppeliusRTX3070Admission = coppeliusRTX3070CapabilityAdmission)
    (coppeliusRTX3070Plan = coppeliusRTX3070BuildPlan))