module Coppelius.Build.Placement

import Compiler.Planning.VA
import Coppelius.ArenaPlan
import Coppelius.Build.Graph
import Hardware.Nvidia.SM86.Command.QMD
import Hardware.Nvidia.SM86.Command.WholeProgramPlan
import Platform.Linux.Nvidia.PlanHost
import Platform.Linux.Nvidia.PlanHostRequest
import Std.Natural

-- ---- the buffers the plan sizes ----
-- Placed after the ones the plan itself depends on (Coppelius.ArenaPlan: the
-- GPFIFO, the staging window, the program region), in the card's address
-- space and in the process: the semaphores, a slot per submission; the QMD
-- buffer; and last the pushbuffer, whose extent is its expansion's (the host
-- learns it from the realization), so nothing is placed by it.  The host
-- side of the arena certificate decides that they are disjoint.

-- one semaphore slot per submission; then the per-launch profile's slots
-- (NvidiaSubmissionScheduleProfiled: a timestamped release after each
-- launch, 16 bytes at its QMD ordinal), reserved in every build so that a
-- profiling build differs from production only in its pushbuffer; to the
-- page
def coppeliusProfileOffset : Nat =
  (naturalMultiply prSemaphoreStride coppeliusSubmissionCount)

def coppeliusProfileSlotBytes : Nat = 16

def coppeliusSemaphoreBytes : Nat =
  (nvidiaPlanHostRoundUp
    (naturalAdd coppeliusProfileOffset (naturalMultiply coppeliusProfileSlotBytes coppeliusLaunchCount))
    nvidiaPlanHostMappingUnit)

-- the plan's submissions, each launch followed by its profile release
def coppeliusProfiledSubmissionSchedule : (family NvidiaSubmissionSchedule) =
  (constructor NvidiaSubmissionSchedule NvidiaSubmissionScheduleProfiled
    coppeliusProfileOffset coppeliusSubmissionSchedule)

-- one GPFIFO entry per submission
def coppeliusGPFIFOTableBytes : Nat =
  (naturalMultiply 8 coppeliusSubmissionCount)

-- the QMD table: a record per launch of the plan at the card's record
-- stride, to the page; parameter blocks the program region cannot hold
-- spill past it
def coppeliusQMDTableBytesFor =
  (lambda unrestricted recordBytes : Nat .
    (nvidiaPlanHostRoundUp (naturalMultiply coppeliusLaunchCount recordBytes) nvidiaPlanHostMappingUnit))

-- the RTX pairings' (QMD V03)
def coppeliusQMDTableBytes : Nat =
  (coppeliusQMDTableBytesFor qmdRecordBytes)

def coppeliusSemaphoreBase : Nat =
  (vaPlaceAfter coppeliusProgramBase coppeliusSM86CompatProgramBytesNatural coppeliusDeviceSpaceAlignment)

def coppeliusQMDBase : Nat =
  (vaPlaceAfter coppeliusSemaphoreBase coppeliusSemaphoreBytes coppeliusDeviceSpaceAlignment)

def coppeliusPushbufferBase : Nat =
  (vaPlaceAfter coppeliusQMDBase coppeliusSM86CompatQMDBytesNatural coppeliusDeviceSpaceAlignment)

def coppeliusHostSemaphores : Nat =
  (vaPlaceAfter coppeliusHostProgram coppeliusSM86CompatProgramBytesNatural nvidiaPlanHostMappingAlignment)

def coppeliusHostQMD : Nat =
  (vaPlaceAfter coppeliusHostSemaphores coppeliusSemaphoreBytes nvidiaPlanHostMappingAlignment)

def coppeliusHostPushbuffer : Nat =
  (vaPlaceAfter coppeliusHostQMD coppeliusSM86CompatQMDBytesNatural nvidiaPlanHostMappingAlignment)

-- the pushbuffer's extent: its expansion, to the mapping unit
def coppeliusPushbufferBytes =
  (lambda unrestricted pushExpanded : Nat .
    (nvidiaPlanHostRoundUp pushExpanded nvidiaPlanHostMappingUnit))