module Coppelius.LaunchPolicy

import Coppelius.SM86Capability
import Hardware.Nvidia.SM86.Command.LaunchBatch
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Std.Physical

-- QMD and pushbuffer bytes continue to come exclusively from the
-- Hardware.Nvidia.SM86.Command.* encoders.  This
-- record freezes the conservative batching and launch limits used by the
-- compatibility artifact; it is not another encoder.
family CoppeliusLaunchPolicy : Type 0
constructor CoppeliusLaunchPolicyValue
field unrestricted coppeliusLaunchProfileIdentity : Bytes
field unrestricted coppeliusLaunchOrdering : (family LaunchOrdering)
field unrestricted coppeliusLaunchQMDRecordBytes : ByteCount
field unrestricted coppeliusLaunchQMDRecordCount : Nat
field unrestricted coppeliusLaunchQMDCapacity : Nat
field unrestricted coppeliusLaunchQMDReferenceCount : Nat
field unrestricted coppeliusLaunchBatchCount : Nat
field unrestricted coppeliusLaunchMaximumGridX : GridDimension
field unrestricted coppeliusLaunchMaximumPushDwords : Nat
field unrestricted coppeliusLaunchFreshTerminalGPFIFOCursor : Nat
field unrestricted coppeliusLaunchDeviceTimestampRequired : Nat
field unrestricted coppeliusLaunchAllowedHostFallbacks : Nat

end-family

def coppeliusSM86CompatQMDRecordBytes : ByteCount =
  (stdByteCount 256)

def coppeliusSM86CompatQMDRecordCount : Nat =
  10_203

def coppeliusSM86CompatQMDCapacity : Nat =
  10_240

def coppeliusSM86CompatQMDReferenceCount : Nat =
  45_915

def coppeliusSM86CompatLaunchBatchCount : Nat =
  511

def coppeliusSM86CompatMaximumPushDwords : Nat =
  2_097_151

def coppeliusSM86CompatFreshTerminalGPFIFOCursor : Nat =
  511

def coppeliusSM86CompatLaunchPolicy : (family CoppeliusLaunchPolicy) =
  (record
    CoppeliusLaunchPolicy
    (coppeliusLaunchProfileIdentity = coppeliusSM86CompatProfileIdentity)
    (coppeliusLaunchOrdering = (constructor LaunchOrdering LaunchWithIdleBarrier))
    (coppeliusLaunchQMDRecordBytes = coppeliusSM86CompatQMDRecordBytes)
    (coppeliusLaunchQMDRecordCount = coppeliusSM86CompatQMDRecordCount)
    (coppeliusLaunchQMDCapacity = coppeliusSM86CompatQMDCapacity)
    (coppeliusLaunchQMDReferenceCount = coppeliusSM86CompatQMDReferenceCount)
    (coppeliusLaunchBatchCount = coppeliusSM86CompatLaunchBatchCount)
    (coppeliusLaunchMaximumGridX = coppeliusSM86CompatMaximumGridX)
    (coppeliusLaunchMaximumPushDwords = coppeliusSM86CompatMaximumPushDwords)
    (coppeliusLaunchFreshTerminalGPFIFOCursor = coppeliusSM86CompatFreshTerminalGPFIFOCursor)
    (coppeliusLaunchDeviceTimestampRequired = 1)
    (coppeliusLaunchAllowedHostFallbacks = 0))