module Hardware.Nvidia.SM86.Command.QMD

import Accelerator.SM86.QMD
import Model.Word32
import Model.Word32Logic
import Model.Word64
import Std.Byte
import Std.Natural
import Model.Config
import Model.Parameter

family QMDErrorCode : Type 0
constructor QMDProgramAddressOutOfRange
constructor QMDScratchAddressOutOfRange
constructor QMDGridDimensionZero
constructor QMDGridYZOutOfRange
constructor QMDBlockDimensionZero
constructor QMDBlockDimensionOutOfRange
constructor QMDBlockVolumeOutOfRange
constructor QMDProgramBytesZero
constructor QMDSharedMemoryOutOfRange
constructor QMDRegisterCountOutOfRange
constructor QMDPrefetchUnitsOutOfRange
constructor QMDConstantBufferAddressOutOfRange
constructor QMDConstantBufferSizeOutOfRange

end-family

family QMDOptionalScratch : Type 0
constructor QMDNoScratch
constructor QMDScratch
field unrestricted qmdScratchAddress : (family ModelWord64)

end-family

-- QMD V03 constant-buffer binding.  This is deliberately separate from the
-- historical OptionalScratch input above: the old owner encoded the address
-- and INVALIDATE bit but did not set CONSTANT_BUFFER_VALID(0), and fixed the
-- size to 64 KiB.  Maintained callers that need a real parameter bank use this
-- explicit address-and-extent contract; the historical API remains stable.
family QMDOptionalConstantBuffer : Type 0
constructor QMDNoConstantBuffer
constructor QMDConstantBuffer
field unrestricted qmdConstantBufferAddress : (family ModelWord64)
field unrestricted qmdConstantBufferBytes : (family ModelWord32)

end-family

family QMDConfig : Type 0
constructor QMDConfigValue
field unrestricted qmdProgramAddress : (family ModelWord64)
field unrestricted qmdProgramBytes : (family ModelWord32)
field unrestricted qmdPrefetchUnits : (family ModelWord32)
field unrestricted qmdGridX : (family ModelWord32)
field unrestricted qmdGridY : (family ModelWord32)
field unrestricted qmdGridZ : (family ModelWord32)
field unrestricted qmdBlockX : (family ModelWord32)
field unrestricted qmdBlockY : (family ModelWord32)
field unrestricted qmdBlockZ : (family ModelWord32)
field unrestricted qmdSharedBytes : (family ModelWord32)
field unrestricted qmdRegisterCount : (family ModelWord32)
field unrestricted qmdOptionalScratch : (family QMDOptionalScratch)

end-family

family QMDValidationResult : Type 0
constructor QMDValidated
constructor QMDRejected
field unrestricted qmdValidationError : (family QMDErrorCode)

end-family

family QMDConstantFields : Type 0
constructor QMDConstantFieldsValue
field unrestricted qmdConstantEnable : (family ModelWord32)
field unrestricted qmdConstantLow : (family ModelWord32)
field unrestricted qmdConstantHigh : (family ModelWord32)

end-family

family QMDBuildResult : Type 0
constructor QMDBuilt
field unrestricted qmdEndodedBytes : Bytes
field unrestricted qmdEncodedDwords : Nat
field unrestricted qmdEncodedAlignment : Nat
field unrestricted qmdHostFallbacks : Nat
constructor QMDBuildRejected
field unrestricted qmdBuildError : (family QMDErrorCode)

end-family

family QMDIdentityBinding : Type 0
constructor QMDIdentityBindingValue
field unrestricted qmdProgramIdentity : Bytes
field unrestricted qmdResourceIdentity : Bytes
field unrestricted qmdConstantIdentity : Bytes

end-family

family QMDAttestationError : Type 0
constructor QMDPrefetchGeometryMismatch
constructor QMDEncodingExtentMismatch
constructor QMDIdentityMalformed
constructor QMDIdentityMismatch
constructor QMDEncodingRejected
field unrestricted qmdEncodingRejectedError : (family QMDErrorCode)

end-family

family QMDAttestedReceipt : Type 0
constructor QMDAttestedReceiptValue
field unrestricted qmdAttestedBytes : Bytes
field unrestricted qmdAttestedBinding : (family QMDIdentityBinding)
field unrestricted qmdAttestedDwords : Nat
field unrestricted qmdAttestedAlignment : Nat
field unrestricted qmdAttestedHostFallbacks : Nat

end-family

family QMDAttestedResult : Type 0
constructor QMDAttested
field unrestricted qmdAttestedReceiptValue : (family QMDAttestedReceipt)
constructor QMDAttestationRejected
field unrestricted qmdAttestationFailure : (family QMDAttestationError)

end-family

-- Field projection (fields do not create definitions).
def qmdRegisterCount =
  (lambda unrestricted value : (family QMDConfig) .
    (eliminate
      QMDConfig
      (lambda unrestricted current : (family QMDConfig) . (family ModelWord32))
      value
      (branch
        QMDConfigValue
        hermesQMDProgramAddress
        hermesQMDProgramBytes
        hermesQMDPrefetchUnits
        hermesQMDGridX
        hermesQMDGridY
        hermesQMDGridZ
        hermesQMDBlockX
        hermesQMDBlockY
        hermesQMDBlockZ
        hermesQMDSharedBytes
        hermesQMDRegisterCountField
        hermesQMDOptionalScratch
        .
        hermesQMDRegisterCountField)))

-- Field projection (fields do not create definitions).
def qmdSharedBytes =
  (lambda unrestricted value : (family QMDConfig) .
    (eliminate
      QMDConfig
      (lambda unrestricted current : (family QMDConfig) . (family ModelWord32))
      value
      (branch
        QMDConfigValue
        hermesQMDProgramAddress
        hermesQMDProgramBytes
        hermesQMDPrefetchUnits
        hermesQMDGridX
        hermesQMDGridY
        hermesQMDGridZ
        hermesQMDBlockX
        hermesQMDBlockY
        hermesQMDBlockZ
        hermesQMDSharedBytesField
        hermesQMDRegisterCount
        hermesQMDOptionalScratch
        .
        hermesQMDSharedBytesField)))

def qmdErrorCodeBytes =
  (lambda unrestricted code : (family QMDErrorCode) .
    (eliminate
      QMDErrorCode
      (lambda unrestricted current : (family QMDErrorCode) . Bytes)
      code
      (branch QMDProgramAddressOutOfRange . b"ALPHA-HQMD-501")
      (branch QMDScratchAddressOutOfRange . b"ALPHA-HQMD-502")
      (branch QMDGridDimensionZero . b"ALPHA-HQMD-503")
      (branch QMDGridYZOutOfRange . b"ALPHA-HQMD-504")
      (branch QMDBlockDimensionZero . b"ALPHA-HQMD-505")
      (branch QMDBlockDimensionOutOfRange . b"ALPHA-HQMD-506")
      (branch QMDBlockVolumeOutOfRange . b"ALPHA-HQMD-507")
      (branch QMDProgramBytesZero . b"ALPHA-HQMD-508")
      (branch QMDSharedMemoryOutOfRange . b"ALPHA-HQMD-509")
      (branch QMDRegisterCountOutOfRange . b"ALPHA-HQMD-510")
      (branch QMDPrefetchUnitsOutOfRange . b"ALPHA-HQMD-511")
      (branch QMDConstantBufferAddressOutOfRange . b"ALPHA-HQMD-512")
      (branch QMDConstantBufferSizeOutOfRange . b"ALPHA-HQMD-513")))

def qmdFlagAnd =
  (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalAnd left right)))

def qmdWord32Positive =
  (lambda unrestricted value : (family ModelWord32) .
    (nat-less-than zero (modelWord32ToNatural value)))

def qmdWord32AtMost =
  (lambda unrestricted value : (family ModelWord32) .
    (lambda unrestricted limit : Nat . (nat-less-than (modelWord32ToNatural value) (succ limit))))

def qmdAddress49 =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      address
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (qmdFlagAnd
          (byte-equal b7 (byte 0))
          (nat-less-than (byte-to-nat b6) (byte-to-nat (byte 2)))))))

def qmdScratchAddressValid =
  (lambda unrestricted scratch : (family QMDOptionalScratch) .
    (eliminate
      QMDOptionalScratch
      (lambda unrestricted current : (family QMDOptionalScratch) . Nat)
      scratch
      (branch QMDNoScratch . (succ zero))
      (branch QMDScratch address . (qmdAddress49 address))))

def qmdThreePositive =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (qmdFlagAnd
          (qmdWord32Positive first)
          (qmdFlagAnd (qmdWord32Positive second) (qmdWord32Positive third))))))

def qmdThreeAtMost =
  (lambda unrestricted first : (family ModelWord32) .
    (lambda unrestricted second : (family ModelWord32) .
      (lambda unrestricted third : (family ModelWord32) .
        (lambda unrestricted limit : Nat .
          (qmdFlagAnd
            (qmdWord32AtMost first limit)
            (qmdFlagAnd (qmdWord32AtMost second limit) (qmdWord32AtMost third limit)))))))

def qmdBlockVolume =
  (lambda unrestricted blockX : (family ModelWord32) .
    (lambda unrestricted blockY : (family ModelWord32) .
      (lambda unrestricted blockZ : (family ModelWord32) .
        (naturalMultiply
          (modelWord32ToNatural blockX)
          (naturalMultiply (modelWord32ToNatural blockY) (modelWord32ToNatural blockZ))))))

def qmdRoundedSharedBytes =
  (lambda unrestricted shared : (family ModelWord32) .
    (modelWord32ShiftLeft
      (modelWord32ShiftRight (modelWord32Add shared 255) (byte-to-nat (byte 8)))
      (byte-to-nat (byte 8))))

def qmdSharedMemoryValid =
  (lambda unrestricted shared : (family ModelWord32) .
    (nat-less-than
      (modelWord32ToNatural (qmdRoundedSharedBytes shared))
      (succ (naturalMultiply (byte-to-nat (byte 99)) (naturalPowerOfTwo (byte-to-nat (byte 10)))))))

def qmdRequire =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted error : (family QMDErrorCode) .
      (lambda unrestricted success : (family QMDValidationResult) .
        (nat-eliminate
          (lambda unrestricted current : Nat . (family QMDValidationResult))
          (constructor QMDValidationResult QMDRejected error)
          (lambda unrestricted predecessor : Nat .
            (lambda unrestricted induction : (family QMDValidationResult) . success))
          condition))))

def qmdValidate =
  (lambda unrestricted config : (family QMDConfig) .
    (eliminate
      QMDConfig
      (lambda unrestricted current : (family QMDConfig) . (family QMDValidationResult))
      config
      (branch
        QMDConfigValue
        programAddress
        programBytes
        prefetchUnits
        gridX
        gridY
        gridZ
        blockX
        blockY
        blockZ
        shared
        registers
        scratch
        .
        (qmdRequire
          (qmdAddress49 programAddress)
          (constructor QMDErrorCode QMDProgramAddressOutOfRange)
          (qmdRequire
            (qmdScratchAddressValid scratch)
            (constructor QMDErrorCode QMDScratchAddressOutOfRange)
            (qmdRequire
              (qmdThreePositive gridX gridY gridZ)
              (constructor QMDErrorCode QMDGridDimensionZero)
              (qmdRequire
                (qmdFlagAnd
                  (qmdWord32AtMost
                    gridY
                    (naturalSaturatingSubtract
                      (naturalPowerOfTwo (byte-to-nat (byte 16)))
                      (succ zero)))
                  (qmdWord32AtMost
                    gridZ
                    (naturalSaturatingSubtract
                      (naturalPowerOfTwo (byte-to-nat (byte 16)))
                      (succ zero))))
                (constructor QMDErrorCode QMDGridYZOutOfRange)
                (qmdRequire
                  (qmdThreePositive blockX blockY blockZ)
                  (constructor QMDErrorCode QMDBlockDimensionZero)
                  (qmdRequire
                    (qmdThreeAtMost
                      blockX
                      blockY
                      blockZ
                      (naturalSaturatingSubtract
                        (naturalPowerOfTwo (byte-to-nat (byte 16)))
                        (succ zero)))
                    (constructor QMDErrorCode QMDBlockDimensionOutOfRange)
                    (qmdRequire
                      (nat-less-than
                        (qmdBlockVolume blockX blockY blockZ)
                        (succ (naturalPowerOfTwo (byte-to-nat (byte 10)))))
                      (constructor QMDErrorCode QMDBlockVolumeOutOfRange)
                      (qmdRequire
                        (qmdWord32Positive programBytes)
                        (constructor QMDErrorCode QMDProgramBytesZero)
                        (qmdRequire
                          (qmdSharedMemoryValid shared)
                          (constructor QMDErrorCode QMDSharedMemoryOutOfRange)
                          (qmdRequire
                            (qmdFlagAnd
                              (qmdWord32Positive registers)
                              (qmdWord32AtMost registers (byte-to-nat (byte 255))))
                            (constructor QMDErrorCode QMDRegisterCountOutOfRange)
                            (qmdRequire
                              (qmdFlagAnd
                                (qmdWord32Positive prefetchUnits)
                                (qmdWord32AtMost
                                  prefetchUnits
                                  (naturalSaturatingSubtract
                                    (naturalPowerOfTwo (byte-to-nat (byte 9)))
                                    (succ zero))))
                              (constructor QMDErrorCode QMDPrefetchUnitsOutOfRange)
                              (constructor QMDValidationResult QMDValidated)))))))))))))))

def qmdPhysicalWord =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family SM86QMDWord32))
      value
      (branch
        ModelWord32Value
        b0
        b1
        b2
        b3
        .
        (constructor SM86QMDWord32 SM86QMDWord32Value b0 b1 b2 b3))))

def qmdProgramAddressLow =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
      address
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))

def qmdProgramAddressHigh =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
      address
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor ModelWord32 ModelWord32Value b4 b5 (byteAnd b6 (byte 1)) (byte 0)))))

def qmdPrefetchBaseShifted =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
      address
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor ModelWord32 ModelWord32Value b1 b2 b3 b4))))

def qmdPrefetchHigh =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
      address
      (branch
        ModelWord64Value
        b0
        b1
        b2
        b3
        b4
        b5
        b6
        b7
        .
        (constructor ModelWord32 ModelWord32Value b5 (byteAnd b6 (byte 1)) (byte 0) (byte 0)))))

def qmdConstantFieldsForScratch =
  (lambda unrestricted scratch : (family QMDOptionalScratch) .
    (eliminate
      QMDOptionalScratch
      (lambda unrestricted current : (family QMDOptionalScratch) . (family QMDConstantFields))
      scratch
      (branch QMDNoScratch . (constructor QMDConstantFields QMDConstantFieldsValue 0 0 0))
      (branch
        QMDScratch
        address
        .
        (constructor
          QMDConstantFields
          QMDConstantFieldsValue
          1
          (qmdProgramAddressLow address)
          (modelWord32Or (qmdProgramAddressHigh address) 2147745792)))))

def qmdConstantBufferAddressValid =
  (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
    (eliminate
      QMDOptionalConstantBuffer
      (lambda unrestricted current : (family QMDOptionalConstantBuffer) . Nat)
      constantBuffer
      (branch QMDNoConstantBuffer . (succ zero))
      (branch QMDConstantBuffer address extent . (qmdAddress49 address))))

-- Constant bank 0 as an SM86 kernel sees it: the driver's words below the
-- parameters (the block's X extent at 0), the kernel's parameters from
-- 0x160.  A launch's parameter block is laid out against these.
def qmdBlockDimensionXOffset : Nat = 0
def qmdKernelParameterBase : Nat = 0x160

-- one launch record in a QMD table
def qmdRecordBytes : Nat = 256

def qmdConstantBufferMaximumBytes : Nat =
  (naturalMultiply
    (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 13))) (succ zero))
    (byte-to-nat (byte 16)))

def qmdConstantBufferSizeValid =
  (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
    (eliminate
      QMDOptionalConstantBuffer
      (lambda unrestricted current : (family QMDOptionalConstantBuffer) . Nat)
      constantBuffer
      (branch QMDNoConstantBuffer . (succ zero))
      (branch
        QMDConstantBuffer
        address
        extent
        .
        (qmdFlagAnd
          (qmdWord32Positive extent)
          (qmdWord32AtMost extent qmdConstantBufferMaximumBytes)))))

-- QMDV03_00 slot zero:
--   dword 32 = ADDRESS_LOWER
--   dword 33 bits 0..16 = ADDRESS_UPPER, bit 18 = INVALIDATE,
--            bits 19..31 = ceil(bytes / 16)
--   dword 20 bit 0 = CONSTANT_BUFFER_VALID(0)
def qmdConstantFieldsForBuffer =
  (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
    (eliminate
      QMDOptionalConstantBuffer
      (lambda unrestricted current : (family QMDOptionalConstantBuffer) .
        (family QMDConstantFields))
      constantBuffer
      (branch QMDNoConstantBuffer . (constructor QMDConstantFields QMDConstantFieldsValue 0 0 0))
      (branch
        QMDConstantBuffer
        address
        extent
        .
        (constructor
          QMDConstantFields
          QMDConstantFieldsValue
          1
          (qmdProgramAddressLow address)
          (modelWord32Or
            (qmdProgramAddressHigh address)
            (modelWord32Or
              262144
              (modelWord32ShiftLeft
                (modelWord32ShiftRight (modelWord32Add extent 15) (byte-to-nat (byte 4)))
                (byte-to-nat (byte 19)))))))))

def qmdSharedField =
  (lambda unrestricted shared : (family ModelWord32) .
    (modelWord32Or (modelWord32Add (qmdRoundedSharedBytes shared) 1024) 879230976))

def qmdBlockXField =
  (lambda unrestricted blockX : (family ModelWord32) .
    (modelWord32Or (modelWord32ShiftLeft blockX (byte-to-nat (byte 16))) 48))

def qmdBlockYZField =
  (lambda unrestricted blockY : (family ModelWord32) .
    (lambda unrestricted blockZ : (family ModelWord32) .
      (modelWord32Or blockY (modelWord32ShiftLeft blockZ (byte-to-nat (byte 16))))))

-- The register field holds the allocation, not the program's count: the
-- registers the program names and the two per-thread registers the hardware
-- reserves (Accelerator.SM86.Operands.sm86ReservedRegisters), in units of
-- eight, as the sm_121 QMD's.  A raw count that is not a multiple of eight
-- leaves the program's highest registers outside the allocated granule:
-- Xid 13 on the RTX 3090 (the tiled product's 164, 2026-09-27).
def qmdAllocatedRegisters =
  (lambda unrestricted registers : (family ModelWord32) .
    (modelWord32ShiftLeft
      (modelWord32ShiftRight (modelWord32Add registers 9) (byte-to-nat (byte 3)))
      (byte-to-nat (byte 3))))

def qmdRegisterField =
  (lambda unrestricted registers : (family ModelWord32) .
    (lambda unrestricted constantEnable : (family ModelWord32) .
      (modelWord32Or
        constantEnable
        (modelWord32Or (modelWord32ShiftLeft (qmdAllocatedRegisters registers) (byte-to-nat (byte 8))) 3407872))))

def qmdPrefetchControl =
  (lambda unrestricted address : (family ModelWord64) .
    (lambda unrestricted units : (family ModelWord32) .
      (modelWord32Or
        (qmdPrefetchHigh address)
        (modelWord32Or (modelWord32ShiftLeft units (byte-to-nat (byte 9))) 2248146944))))

-- QMD v03 is shared by SM86 and SM89.  The upper byte of this word is the
-- target SASS architecture tag; keep it explicit for compatible binaries
-- launched through a different compute class.
def qmdPrefetchControlForArchitecture =
  (lambda unrestricted architecture : (family ModelWord32) .
    (lambda unrestricted address : (family ModelWord64) .
      (lambda unrestricted units : (family ModelWord32) .
        (modelWord32Or
          (qmdPrefetchHigh address)
          (modelWord32Or
            (modelWord32ShiftLeft units (byte-to-nat (byte 9)))
            (modelWord32ShiftLeft architecture (byte-to-nat (byte 24))))))))

def qmdBuildPhysicalConfig =
  (lambda unrestricted config : (family QMDConfig) .
    (eliminate
      QMDConfig
      (lambda unrestricted current : (family QMDConfig) . (family SM86QMDPhysicalConfig))
      config
      (branch
        QMDConfigValue
        programAddress
        programBytes
        prefetchUnits
        gridX
        gridY
        gridZ
        blockX
        blockY
        blockZ
        shared
        registers
        scratch
        .
        (eliminate
          QMDConstantFields
          (lambda unrestricted current : (family QMDConstantFields) .
            (family SM86QMDPhysicalConfig))
          (qmdConstantFieldsForScratch scratch)
          (branch
            QMDConstantFieldsValue
            constantEnable
            constantLow
            constantHigh
            .
            (constructor
              SM86QMDPhysicalConfig
              SM86QMDPhysicalConfigValue
              (qmdPhysicalWord (qmdPrefetchBaseShifted programAddress))
              (qmdPhysicalWord gridX)
              (qmdPhysicalWord gridY)
              (qmdPhysicalWord gridZ)
              (qmdPhysicalWord (qmdSharedField shared))
              (qmdPhysicalWord (qmdBlockXField blockX))
              (qmdPhysicalWord (qmdBlockYZField blockY blockZ))
              (qmdPhysicalWord (qmdRegisterField registers constantEnable))
              (qmdPhysicalWord constantLow)
              (qmdPhysicalWord constantHigh)
              (qmdPhysicalWord (qmdProgramAddressLow programAddress))
              (qmdPhysicalWord (qmdProgramAddressHigh programAddress))
              (qmdPhysicalWord (qmdPrefetchControl programAddress prefetchUnits))))))))

def qmdBuildPhysicalConfigWithConstantBufferForArchitecture =
  (lambda unrestricted architecture : (family ModelWord32) .
    (lambda unrestricted config : (family QMDConfig) .
      (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
      (eliminate
        QMDConfig
        (lambda unrestricted current : (family QMDConfig) . (family SM86QMDPhysicalConfig))
        config
        (branch
          QMDConfigValue
          programAddress
          programBytes
          prefetchUnits
          gridX
          gridY
          gridZ
          blockX
          blockY
          blockZ
          shared
          registers
          scratch
          .
          (eliminate
            QMDConstantFields
            (lambda unrestricted current : (family QMDConstantFields) .
              (family SM86QMDPhysicalConfig))
            (qmdConstantFieldsForBuffer constantBuffer)
            (branch
              QMDConstantFieldsValue
              constantEnable
              constantLow
              constantHigh
              .
              (constructor
                SM86QMDPhysicalConfig
                SM86QMDPhysicalConfigValue
                (qmdPhysicalWord (qmdPrefetchBaseShifted programAddress))
                (qmdPhysicalWord gridX)
                (qmdPhysicalWord gridY)
                (qmdPhysicalWord gridZ)
                (qmdPhysicalWord (qmdSharedField shared))
                (qmdPhysicalWord (qmdBlockXField blockX))
                (qmdPhysicalWord (qmdBlockYZField blockY blockZ))
                (qmdPhysicalWord (qmdRegisterField registers constantEnable))
                (qmdPhysicalWord constantLow)
                (qmdPhysicalWord constantHigh)
                (qmdPhysicalWord (qmdProgramAddressLow programAddress))
                (qmdPhysicalWord (qmdProgramAddressHigh programAddress))
                (qmdPhysicalWord
                  (qmdPrefetchControlForArchitecture
                    architecture
                    programAddress
                    prefetchUnits))))))))))

def qmdBuildPhysicalConfigWithConstantBuffer =
  (lambda unrestricted config : (family QMDConfig) .
    (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
      (qmdBuildPhysicalConfigWithConstantBufferForArchitecture
        (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
        config
        constantBuffer)))

def qmdBuild =
  (lambda unrestricted config : (family QMDConfig) .
    (eliminate
      QMDValidationResult
      (lambda unrestricted current : (family QMDValidationResult) . (family QMDBuildResult))
      (qmdValidate config)
      (branch
        QMDValidated
        .
        (constructor
          QMDBuildResult
          QMDBuilt
          (sm86EncodeQMD (qmdBuildPhysicalConfig config))
          (byte-to-nat (byte 64))
          (succ (byte-to-nat (byte 255)))
          zero))
      (branch QMDRejected error . (constructor QMDBuildResult QMDBuildRejected error))))

def qmdBuildWithConstantBufferForArchitecture =
  (lambda unrestricted architecture : (family ModelWord32) .
    (lambda unrestricted config : (family QMDConfig) .
      (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
      (eliminate
        QMDValidationResult
        (lambda unrestricted current : (family QMDValidationResult) . (family QMDBuildResult))
        (qmdValidate config)
        (branch
          QMDValidated
          .
          (nat-eliminate
            (lambda unrestricted addressValid : Nat . (family QMDBuildResult))
            (constructor
              QMDBuildResult
              QMDBuildRejected
              (constructor QMDErrorCode QMDConstantBufferAddressOutOfRange))
            (lambda unrestricted addressPredecessor : Nat .
              (lambda unrestricted addressInduction : (family QMDBuildResult) .
                (nat-eliminate
                  (lambda unrestricted sizeValid : Nat . (family QMDBuildResult))
                  (constructor
                    QMDBuildResult
                    QMDBuildRejected
                    (constructor QMDErrorCode QMDConstantBufferSizeOutOfRange))
                  (lambda unrestricted sizePredecessor : Nat .
                    (lambda unrestricted sizeInduction : (family QMDBuildResult) .
                      (constructor
                        QMDBuildResult
                        QMDBuilt
                        (sm86EncodeQMD
                          (qmdBuildPhysicalConfigWithConstantBufferForArchitecture
                            architecture config constantBuffer))
                        (byte-to-nat (byte 64))
                        (succ (byte-to-nat (byte 255)))
                        zero)))
                  (qmdConstantBufferSizeValid constantBuffer))))
            (qmdConstantBufferAddressValid constantBuffer)))
        (branch QMDRejected error . (constructor QMDBuildResult QMDBuildRejected error))))))

def qmdBuildWithConstantBuffer =
  (lambda unrestricted config : (family QMDConfig) .
    (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
      (qmdBuildWithConstantBufferForArchitecture
        (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
        config
        constantBuffer)))

-- The Stage-0 oracle derives prefetch units from the unaligned program start
-- and byte extent. A supplied value is accepted only when it is identical.
def qmdProgramLowByteNatural =
  (lambda unrestricted address : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Nat)
      address
      (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-to-nat b0))))

def qmdExpectedPrefetchUnitsNatural =
  (lambda unrestricted address : (family ModelWord64) .
    (lambda unrestricted programBytes : (family ModelWord32) .
      (app
        (lambda unrestricted requested : Nat .
          (nat-eliminate
            (lambda unrestricted aboveMaximum : Nat . Nat)
            requested
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : Nat .
                (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 9))) (succ zero))))
            (nat-less-than
              (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 9))) (succ zero))
              requested)))
        (naturalDivideUnchecked
          (naturalAdd
            (naturalAdd (qmdProgramLowByteNatural address) (modelWord32ToNatural programBytes))
            (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 8))) (succ zero)))
          (naturalPowerOfTwo (byte-to-nat (byte 8)))))))

def qmdPrefetchGeometryMatches =
  (lambda unrestricted config : (family QMDConfig) .
    (eliminate
      QMDConfig
      (lambda unrestricted current : (family QMDConfig) . Nat)
      config
      (branch
        QMDConfigValue
        programAddress
        programBytes
        prefetchUnits
        gridX
        gridY
        gridZ
        blockX
        blockY
        blockZ
        shared
        registers
        scratch
        .
        (naturalEqual
          (modelWord32ToNatural prefetchUnits)
          (qmdExpectedPrefetchUnitsNatural programAddress programBytes)))))

def qmdIdentityBindingValid =
  (lambda unrestricted binding : (family QMDIdentityBinding) .
    (eliminate
      QMDIdentityBinding
      (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
      binding
      (branch
        QMDIdentityBindingValue
        program
        resource
        constant
        .
        (naturalAnd
          (naturalEqual (bytes-length program) (byte-to-nat (byte 64)))
          (naturalAnd
            (naturalEqual (bytes-length resource) (byte-to-nat (byte 64)))
            (naturalEqual (bytes-length constant) (byte-to-nat (byte 64))))))))

def qmdIdentityBindingEqual =
  (lambda unrestricted expected : (family QMDIdentityBinding) .
    (lambda unrestricted observed : (family QMDIdentityBinding) .
      (eliminate
        QMDIdentityBinding
        (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
        expected
        (branch
          QMDIdentityBindingValue
          expectedProgram
          expectedResource
          expectedConstant
          .
          (eliminate
            QMDIdentityBinding
            (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
            observed
            (branch
              QMDIdentityBindingValue
              observedProgram
              observedResource
              observedConstant
              .
              (naturalAnd
                (bytes-equal expectedProgram observedProgram)
                (naturalAnd
                  (bytes-equal expectedResource observedResource)
                  (bytes-equal expectedConstant observedConstant)))))))))

def qmdAttestationErrorBytes =
  (lambda unrestricted error : (family QMDAttestationError) .
    (eliminate
      QMDAttestationError
      (lambda unrestricted current : (family QMDAttestationError) . Bytes)
      error
      (branch QMDPrefetchGeometryMismatch . b"ALPHA-HQAT-101")
      (branch QMDEncodingExtentMismatch . b"ALPHA-HQAT-102")
      (branch QMDIdentityMalformed . b"ALPHA-HQAT-103")
      (branch QMDIdentityMismatch . b"ALPHA-HQAT-104")
      (branch QMDEncodingRejected cause . (qmdErrorCodeBytes cause))))

def qmdBuildAttested =
  (lambda unrestricted expected : (family QMDIdentityBinding) .
    (lambda unrestricted observed : (family QMDIdentityBinding) .
      (lambda unrestricted config : (family QMDConfig) .
        (nat-eliminate
          (lambda unrestricted identitiesValid : Nat . (family QMDAttestedResult))
          (constructor
            QMDAttestedResult
            QMDAttestationRejected
            (constructor QMDAttestationError QMDIdentityMalformed))
          (lambda unrestricted validPredecessor : Nat .
            (lambda unrestricted validInduction : (family QMDAttestedResult) .
              (nat-eliminate
                (lambda unrestricted identitiesMatch : Nat . (family QMDAttestedResult))
                (constructor
                  QMDAttestedResult
                  QMDAttestationRejected
                  (constructor QMDAttestationError QMDIdentityMismatch))
                (lambda unrestricted matchPredecessor : Nat .
                  (lambda unrestricted matchInduction : (family QMDAttestedResult) .
                    (nat-eliminate
                      (lambda unrestricted geometryMatches : Nat . (family QMDAttestedResult))
                      (constructor
                        QMDAttestedResult
                        QMDAttestationRejected
                        (constructor QMDAttestationError QMDPrefetchGeometryMismatch))
                      (lambda unrestricted geometryPredecessor : Nat .
                        (lambda unrestricted geometryInduction : (family QMDAttestedResult) .
                          (eliminate
                            QMDBuildResult
                            (lambda unrestricted current : (family QMDBuildResult) .
                              (family QMDAttestedResult))
                            (qmdBuild config)
                            (branch
                              QMDBuilt
                              encoded
                              dwords
                              alignment
                              hostFallbacks
                              .
                              (nat-eliminate
                                (lambda unrestricted exactExtent : Nat . (family QMDAttestedResult))
                                (constructor
                                  QMDAttestedResult
                                  QMDAttestationRejected
                                  (constructor QMDAttestationError QMDEncodingExtentMismatch))
                                (lambda unrestricted extentPredecessor : Nat .
                                  (lambda unrestricted extentInduction : (family QMDAttestedResult) .
                                    (constructor
                                      QMDAttestedResult
                                      QMDAttested
                                      (constructor
                                        QMDAttestedReceipt
                                        QMDAttestedReceiptValue
                                        encoded
                                        observed
                                        dwords
                                        alignment
                                        hostFallbacks))))
                                (naturalEqual
                                  (bytes-length encoded)
                                  (naturalPowerOfTwo (byte-to-nat (byte 8))))))
                            (branch
                              QMDBuildRejected
                              cause
                              .
                              (constructor
                                QMDAttestedResult
                                QMDAttestationRejected
                                (constructor QMDAttestationError QMDEncodingRejected cause))))))
                      (qmdPrefetchGeometryMatches config))))
                (qmdIdentityBindingEqual expected observed))))
          (naturalAnd (qmdIdentityBindingValid expected) (qmdIdentityBindingValid observed))))))