module Accelerator.SM86.Capability

import Model.Parameter
import Model.Word64
import Std.Natural

-- Capability admission is deliberately independent of marketing product names.
-- A caller supplies measured device/runtime facts; a system supplies the exact
-- minimums it needs.  Product name, UUID, PCI identity and driver version belong
-- in the physical receipt that accompanies these facts, not in admission.
family SM86DeviceCapabilities : Type 0
constructor SM86DeviceCapabilitiesValue
field unrestricted sm86CapabilityComputeMajor : Nat
field unrestricted sm86CapabilityComputeMinor : Nat
field unrestricted sm86CapabilityTotalVideoMemoryBytes : (family ModelWord64)
field unrestricted sm86CapabilityAvailableVideoMemoryBytes : (family ModelWord64)
field unrestricted sm86CapabilityMappedAddressEnd : (family ModelWord64)
field unrestricted sm86CapabilityMaximumGridX : Nat
field unrestricted sm86CapabilityUVMSupported : Nat
field unrestricted sm86CapabilityResourceManagerSupported : Nat
field unrestricted sm86CapabilityQMDSupported : Nat
field unrestricted sm86CapabilityPushbufferSupported : Nat
field unrestricted sm86CapabilityGPFIFOSupported : Nat
field unrestricted sm86CapabilityDeviceTimestampsSupported : Nat
field unrestricted sm86CapabilityHostFallbacks : Nat

end-family

family SM86CapabilityRequirements : Type 0
constructor SM86CapabilityRequirementsValue
field unrestricted sm86RequirementComputeMajor : Nat
field unrestricted sm86RequirementComputeMinor : Nat
field unrestricted sm86RequirementAvailableVideoMemoryBytes : (family ModelWord64)
field unrestricted sm86RequirementMappedAddressEnd : (family ModelWord64)
field unrestricted sm86RequirementMaximumGridX : Nat
field unrestricted sm86RequirementUVM : Nat
field unrestricted sm86RequirementResourceManager : Nat
field unrestricted sm86RequirementQMD : Nat
field unrestricted sm86RequirementPushbuffer : Nat
field unrestricted sm86RequirementGPFIFO : Nat
field unrestricted sm86RequirementDeviceTimestamps : Nat
field unrestricted sm86RequirementNoHostFallback : Nat

end-family

family SM86CapabilityChecks : Type 0
constructor SM86CapabilityChecksValue
field unrestricted sm86CapabilityArchitectureAccepted : Nat
field unrestricted sm86CapabilityMemoryAccepted : Nat
field unrestricted sm86CapabilityAddressExtentAccepted : Nat
field unrestricted sm86CapabilityGridAccepted : Nat
field unrestricted sm86CapabilityUVMAccepted : Nat
field unrestricted sm86CapabilityResourceManagerAccepted : Nat
field unrestricted sm86CapabilityQMDAccepted : Nat
field unrestricted sm86CapabilityPushbufferAccepted : Nat
field unrestricted sm86CapabilityGPFIFOAccepted : Nat
field unrestricted sm86CapabilityDeviceTimestampsAccepted : Nat
field unrestricted sm86CapabilityNoHostFallbackAccepted : Nat

end-family

family SM86CapabilityAdmission : Type 0
constructor SM86CapabilityAccepted
field unrestricted sm86CapabilityAcceptedChecks : (family SM86CapabilityChecks)
constructor SM86CapabilityRejected
field unrestricted sm86CapabilityRejectedChecks : (family SM86CapabilityChecks)

end-family

def sm86CapabilityOne : Nat =
  (succ zero)

-- Static shared memory needs no per-kernel opt-in QMD setting on SM86. A
-- planner that wants more must establish and encode the dynamic allocation.
def sm86StaticSharedBytesPerBlock : Nat = (naturalMultiply 48 1024)

def sm86CapabilityFlagAccepted =
  (lambda unrestricted value : Nat . (naturalEqual value sm86CapabilityOne))

def sm86CapabilityWord64AtLeast =
  (lambda unrestricted observed : (family ModelWord64) .
    (lambda unrestricted required : (family ModelWord64) .
      (naturalIsZero (modelWord64LessThan observed required))))

def sm86CapabilityChecks =
  (lambda unrestricted requirements : (family SM86CapabilityRequirements) .
    (lambda unrestricted observed : (family SM86DeviceCapabilities) .
      (eliminate
        SM86CapabilityRequirements
        (lambda unrestricted current : (family SM86CapabilityRequirements) .
          (family SM86CapabilityChecks))
        requirements
        (branch
          SM86CapabilityRequirementsValue
          requiredMajor
          requiredMinor
          requiredMemory
          requiredAddressEnd
          requiredGridX
          requiredUVM
          requiredRM
          requiredQMD
          requiredPushbuffer
          requiredGPFIFO
          requiredTimestamps
          requiredNoFallback
          .
          (eliminate
            SM86DeviceCapabilities
            (lambda unrestricted current : (family SM86DeviceCapabilities) .
              (family SM86CapabilityChecks))
            observed
            (branch
              SM86DeviceCapabilitiesValue
              observedMajor
              observedMinor
              observedTotalMemory
              observedAvailableMemory
              observedAddressEnd
              observedGridX
              observedUVM
              observedRM
              observedQMD
              observedPushbuffer
              observedGPFIFO
              observedTimestamps
              observedFallbacks
              .
              (constructor
                SM86CapabilityChecks
                SM86CapabilityChecksValue
                (naturalAnd
                  (naturalEqual observedMajor requiredMajor)
                  (naturalEqual observedMinor requiredMinor))
                (sm86CapabilityWord64AtLeast observedAvailableMemory requiredMemory)
                (sm86CapabilityWord64AtLeast observedAddressEnd requiredAddressEnd)
                (naturalLessOrEqual requiredGridX observedGridX)
                (naturalEqual (sm86CapabilityFlagAccepted observedUVM) requiredUVM)
                (naturalEqual (sm86CapabilityFlagAccepted observedRM) requiredRM)
                (naturalEqual (sm86CapabilityFlagAccepted observedQMD) requiredQMD)
                (naturalEqual (sm86CapabilityFlagAccepted observedPushbuffer) requiredPushbuffer)
                (naturalEqual (sm86CapabilityFlagAccepted observedGPFIFO) requiredGPFIFO)
                (naturalEqual (sm86CapabilityFlagAccepted observedTimestamps) requiredTimestamps)
                (naturalEqual (naturalIsZero observedFallbacks) requiredNoFallback))))))))

def sm86CapabilityChecksAccepted =
  (lambda unrestricted checks : (family SM86CapabilityChecks) .
    (eliminate
      SM86CapabilityChecks
      (lambda unrestricted current : (family SM86CapabilityChecks) . Nat)
      checks
      (branch
        SM86CapabilityChecksValue
        architecture
        memory
        addressExtent
        grid
        uvm
        resourceManager
        qmd
        pushbuffer
        gpfifo
        timestamps
        noFallback
        .
        (naturalAnd
          architecture
          (naturalAnd
            memory
            (naturalAnd
              addressExtent
              (naturalAnd
                grid
                (naturalAnd
                  uvm
                  (naturalAnd
                    resourceManager
                    (naturalAnd
                      qmd
                      (naturalAnd pushbuffer (naturalAnd gpfifo (naturalAnd timestamps noFallback)))))))))))))

def sm86CapabilityAdmit =
  (lambda unrestricted requirements : (family SM86CapabilityRequirements) .
    (lambda unrestricted observed : (family SM86DeviceCapabilities) .
      (app
        (lambda unrestricted checks : (family SM86CapabilityChecks) .
          (nat-eliminate
            (lambda unrestricted accepted : Nat . (family SM86CapabilityAdmission))
            (constructor SM86CapabilityAdmission SM86CapabilityRejected checks)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family SM86CapabilityAdmission) .
                (constructor SM86CapabilityAdmission SM86CapabilityAccepted checks)))
            (sm86CapabilityChecksAccepted checks)))
        (sm86CapabilityChecks requirements observed))))

def sm86CapabilityAdmissionAccepted =
  (lambda unrestricted admission : (family SM86CapabilityAdmission) .
    (eliminate
      SM86CapabilityAdmission
      (lambda unrestricted current : (family SM86CapabilityAdmission) . Nat)
      admission
      (branch SM86CapabilityAccepted checks . sm86CapabilityOne)
      (branch SM86CapabilityRejected checks . zero)))