module Platform.AArch64.HostCapability

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

-- Host-CPU capability admission for an AArch64 build or execution host.  It
-- mirrors Accelerator.SM86.Capability: a caller supplies measured facts, a
-- system supplies exact minimums, and marketing names, hostnames, kernel and
-- driver strings stay in the physical receipt, never in admission.  Core
-- identity is carried as the raw MIDR_EL1 implementer and part fields so that
-- a heterogeneous (performance + efficiency) cluster is described without a
-- product-name field.
family AArch64HostCapabilities : Type 0
constructor AArch64HostCapabilitiesValue
field unrestricted aarch64HostImplementer : Nat
field unrestricted aarch64HostPerformanceCorePart : Nat
field unrestricted aarch64HostPerformanceCoreCount : Nat
field unrestricted aarch64HostEfficiencyCorePart : Nat
field unrestricted aarch64HostEfficiencyCoreCount : Nat
field unrestricted aarch64HostTotalMemoryBytes : (family ModelWord64)
field unrestricted aarch64HostPageSizeBytes : Nat
field unrestricted aarch64HostLevel2CacheBytes : (family ModelWord64)
field unrestricted aarch64HostLevel3CacheBytes : (family ModelWord64)
field unrestricted aarch64HostUnifiedMemory : Nat
field unrestricted aarch64HostFallbacks : Nat

end-family

family AArch64HostRequirements : Type 0
constructor AArch64HostRequirementsValue
field unrestricted aarch64RequirementImplementer : Nat
field unrestricted aarch64RequirementMinimumCores : Nat
field unrestricted aarch64RequirementMinimumMemoryBytes : (family ModelWord64)
field unrestricted aarch64RequirementPageSizeBytes : Nat
field unrestricted aarch64RequirementNoHostFallback : Nat

end-family

family AArch64HostChecks : Type 0
constructor AArch64HostChecksValue
field unrestricted aarch64HostImplementerAccepted : Nat
field unrestricted aarch64HostCoreCountAccepted : Nat
field unrestricted aarch64HostMemoryAccepted : Nat
field unrestricted aarch64HostPageSizeAccepted : Nat
field unrestricted aarch64HostNoFallbackAccepted : Nat

end-family

family AArch64HostAdmission : Type 0
constructor AArch64HostAccepted
field unrestricted aarch64HostAcceptedChecks : (family AArch64HostChecks)
constructor AArch64HostRejected
field unrestricted aarch64HostRejectedChecks : (family AArch64HostChecks)

end-family

def aarch64HostOne : Nat =
  (succ zero)

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

def aarch64HostChecks =
  (lambda unrestricted requirements : (family AArch64HostRequirements) .
    (lambda unrestricted observed : (family AArch64HostCapabilities) .
      (eliminate
        AArch64HostRequirements
        (lambda unrestricted current : (family AArch64HostRequirements) .
          (family AArch64HostChecks))
        requirements
        (branch
          AArch64HostRequirementsValue
          requiredImplementer
          requiredCores
          requiredMemory
          requiredPageSize
          requiredNoFallback
          .
          (eliminate
            AArch64HostCapabilities
            (lambda unrestricted current : (family AArch64HostCapabilities) .
              (family AArch64HostChecks))
            observed
            (branch
              AArch64HostCapabilitiesValue
              observedImplementer
              observedPerformancePart
              observedPerformanceCount
              observedEfficiencyPart
              observedEfficiencyCount
              observedMemory
              observedPageSize
              observedLevel2
              observedLevel3
              observedUnified
              observedFallbacks
              .
              (constructor
                AArch64HostChecks
                AArch64HostChecksValue
                (naturalEqual observedImplementer requiredImplementer)
                (naturalLessOrEqual
                  requiredCores
                  (naturalAdd observedPerformanceCount observedEfficiencyCount))
                (aarch64HostWord64AtLeast observedMemory requiredMemory)
                (naturalEqual observedPageSize requiredPageSize)
                (naturalEqual (naturalIsZero observedFallbacks) requiredNoFallback))))))))

def aarch64HostChecksAccepted =
  (lambda unrestricted checks : (family AArch64HostChecks) .
    (eliminate
      AArch64HostChecks
      (lambda unrestricted current : (family AArch64HostChecks) . Nat)
      checks
      (branch
        AArch64HostChecksValue
        implementer
        coreCount
        memory
        pageSize
        noFallback
        .
        (naturalAnd
          implementer
          (naturalAnd coreCount (naturalAnd memory (naturalAnd pageSize noFallback)))))))

def aarch64HostAdmit =
  (lambda unrestricted requirements : (family AArch64HostRequirements) .
    (lambda unrestricted observed : (family AArch64HostCapabilities) .
      (app
        (lambda unrestricted checks : (family AArch64HostChecks) .
          (nat-eliminate
            (lambda unrestricted accepted : Nat . (family AArch64HostAdmission))
            (constructor AArch64HostAdmission AArch64HostRejected checks)
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (family AArch64HostAdmission) .
                (constructor AArch64HostAdmission AArch64HostAccepted checks)))
            (aarch64HostChecksAccepted checks)))
        (aarch64HostChecks requirements observed))))

def aarch64HostAdmissionAccepted =
  (lambda unrestricted admission : (family AArch64HostAdmission) .
    (eliminate
      AArch64HostAdmission
      (lambda unrestricted current : (family AArch64HostAdmission) . Nat)
      admission
      (branch AArch64HostAccepted checks . aarch64HostOne)
      (branch AArch64HostRejected checks . zero)))