module Platform.DGXSpark.Profile

import Accelerator.SM86.Capability
import Model.Parameter
import Model.Word64
import Platform.AArch64.HostCapability
import Std.Natural
import Std.Physical
import Std.Word

-- The one measured DGX Spark (NVIDIA GB10, product GX10) profile.  Every value
-- here was read on 2026-09-18 from the host recorded in
-- evidence/hardware/dgx-spark-20260918/ (lscpu, /proc/cpuinfo, /proc/meminfo,
-- getconf PAGESIZE, nvidia-smi -q).  Hostname, kernel, driver and product
-- strings live in Platform.DGXSpark.PhysicalInventory as evidence only.
def dgxSparkProfileIdentity : Bytes =
  b"dgx-spark-bringup-v1"

-- MIDR_EL1 implementer 0x41 (Arm Ltd); parts 0xd85 (Cortex-X925) and 0xd87
-- (Cortex-A725), ten cores each, one NUMA node.
def dgxSparkArmImplementer : Nat =
  65

def dgxSparkPerformanceCorePart : Nat =
  3461

def dgxSparkPerformanceCoreCount : Nat =
  10

def dgxSparkEfficiencyCorePart : Nat =
  3463

def dgxSparkEfficiencyCoreCount : Nat =
  10

-- /proc/meminfo MemTotal 127,535,204 kB = 130,596,048,896 bytes of unified
-- CPU/GPU memory; there is no dedicated video memory (nvidia-smi reports N/A).
def dgxSparkTotalMemory : ByteCount =
  (stdByteCount 0x0000_001E_6821_9000)

def dgxSparkPageSize : Nat =
  4096

def dgxSparkLevel2Cache : ByteCount =
  (stdByteCount 0x0000_0000_0190_0000)

def dgxSparkLevel3Cache : ByteCount =
  (stdByteCount 0x0000_0000_0180_0000)

def dgxSparkHostObservation : (family AArch64HostCapabilities) =
  (constructor
    AArch64HostCapabilities
    AArch64HostCapabilitiesValue
    dgxSparkArmImplementer
    dgxSparkPerformanceCorePart
    dgxSparkPerformanceCoreCount
    dgxSparkEfficiencyCorePart
    dgxSparkEfficiencyCoreCount
    (stdByteCountValue dgxSparkTotalMemory)
    dgxSparkPageSize
    (stdByteCountValue dgxSparkLevel2Cache)
    (stdByteCountValue dgxSparkLevel3Cache)
    1
    0)

-- What the Alpha Stage-0 tree needs from an AArch64 build host: Arm cores, at
-- least sixteen of them, at least 64 GiB (the release build of the Coppelius
-- host emitter peaked at 7.9 GB RSS), 4 KiB pages, and no host fallback.
def dgxSparkBuildHostMinimumMemory : ByteCount =
  (stdByteCount 0x0000_0010_0000_0000)

def dgxSparkBuildHostRequirements : (family AArch64HostRequirements) =
  (constructor
    AArch64HostRequirements
    AArch64HostRequirementsValue
    dgxSparkArmImplementer
    16
    (stdByteCountValue dgxSparkBuildHostMinimumMemory)
    dgxSparkPageSize
    1)

def dgxSparkBuildHostAdmit =
  (lambda unrestricted observed : (family AArch64HostCapabilities) .
    (aarch64HostAdmit dgxSparkBuildHostRequirements observed))

-- The GB10 seen through the SM86 capability lens.  Compute capability 12.1
-- (Blackwell); no dedicated video memory; QMD, pushbuffer and GPFIFO support
-- are recorded as zero because no Alpha owner has demonstrated them on this
-- architecture.  Any SM86 requirement must reject this observation: the
-- accepted SM86 artifacts do not run here, and that is a fact of the profile,
-- not a fallback.
def dgxSparkDeviceComputeMajor : Nat =
  12

def dgxSparkDeviceComputeMinor : Nat =
  1

def dgxSparkDeviceObservationSM86 : (family SM86DeviceCapabilities) =
  (constructor
    SM86DeviceCapabilities
    SM86DeviceCapabilitiesValue
    dgxSparkDeviceComputeMajor
    dgxSparkDeviceComputeMinor
    modelWord64Zero
    modelWord64Zero
    modelWord64Zero
    1024
    1
    1
    0
    0
    0
    1
    0)