module Hardware.Nvidia.SM86.Command.LaunchBatch

import Hardware.Nvidia.SM86.Command.Pushbuffer
import Model.Word32
import Model.Word64
import Std.Natural
import Model.Config
import Model.Parameter

family LaunchOrdering : Type 0
constructor LaunchWithIdleBarrier
constructor LaunchWithSemaphore
field unrestricted launchSemaphoreAddress : (family ModelWord64)
field unrestricted launchFirstSemaphorePayload : (family ModelWord32)
constructor LaunchInChannelOrder

end-family

family LaunchAddressList : Type 0
constructor LaunchAddressEnd
constructor LaunchAddressNext
field unrestricted launchAddressHead : (family ModelWord64)
recursive unrestricted launchAddressTail

end-family

family LaunchBatchErrorCode : Type 0
constructor LaunchBatchLimitZero
constructor LaunchAddressSetEmpty
constructor LaunchPayloadRangeWraps
constructor LaunchExceedsBatchLimit
constructor LaunchPushbufferRejected
field unrestricted launchPushbufferError : (family PushbufferErrorCode)

end-family

family LaunchCommandUnit : Type 0
constructor LaunchCommandUnitValue
field unrestricted launchCommandBytes : Bytes
field unrestricted launchCommandDwords : Nat

end-family

family LaunchCommandUnits : Type 0
constructor LaunchCommandUnitsEnd
constructor LaunchCommandUnitsNext
field unrestricted launchCommandUnitHead : (family LaunchCommandUnit)
recursive unrestricted launchCommandUnitTail

end-family

family LaunchCommandUnitsResult : Type 0
constructor LaunchCommandUnitsReady
field unrestricted launchReadyCommandUnits : (family LaunchCommandUnits)
constructor LaunchCommandUnitsRejected
field unrestricted launchCommandUnitsError : (family LaunchBatchErrorCode)

end-family

family LaunchBatch : Type 0
constructor LaunchBatchValue
field unrestricted launchBatchBytes : Bytes
field unrestricted launchBatchDwords : Nat

end-family

family LaunchBatches : Type 0
constructor LaunchBatchesEnd
constructor LaunchBatchesNext
field unrestricted launchBatchHead : (family LaunchBatch)
recursive unrestricted launchBatchTail

end-family

family LaunchPackResult : Type 0
constructor LaunchPackReady
field unrestricted launchPackedBatches : (family LaunchBatches)
constructor LaunchPackRejected
field unrestricted launchPackError : (family LaunchBatchErrorCode)

end-family

family LaunchBatchTelemetry : Type 0
constructor LaunchBatchTelemetryValue
field unrestricted launchBatchTelemetryLaunches : Nat
field unrestricted launchBatchTelemetryBatches : Nat
field unrestricted launchBatchTelemetryHostFallbacks : Nat

end-family

family LaunchBatchResult : Type 0
constructor LaunchBatchesReady
field unrestricted launchReadyBatches : (family LaunchBatches)
field unrestricted launchBatchSuccessTelemetry : (family LaunchBatchTelemetry)
constructor LaunchBatchesRejected
field unrestricted launchBatchFailure : (family LaunchBatchErrorCode)

end-family

family LaunchPhysicalIdentityBinding : Type 0
constructor LaunchPhysicalIdentityBindingValue
field unrestricted launchPhysicalProgramIdentity : Bytes
field unrestricted launchPhysicalResourceIdentity : Bytes
field unrestricted launchPhysicalConstantIdentity : Bytes

end-family

family LaunchPhysicalReceipt : Type 0
constructor LaunchPhysicalReceiptValue
field unrestricted launchPhysicalReceiptIdentity : Bytes
field unrestricted launchPhysicalReceiptBinding : (family LaunchPhysicalIdentityBinding)
field unrestricted launchPhysicalExpectedLaunches : Nat
field unrestricted launchPhysicalSubmittedLaunches : Nat
field unrestricted launchPhysicalRetiredLaunches : Nat
field unrestricted launchPhysicalFinalTimestampLE64 : Bytes
field unrestricted launchPhysicalHostFallbacks : Nat

end-family

family LaunchPhysicalReceiptResult : Type 0
constructor LaunchPhysicalReceiptAccepted
field unrestricted launchAcceptedPhysicalReceipt : (family LaunchPhysicalReceipt)
constructor LaunchPhysicalReceiptRejected
field unrestricted launchPhysicalReceiptFailure : (family LaunchBatchErrorCode)

end-family

def launchBatchErrorCodeBytes =
  (lambda unrestricted code : (family LaunchBatchErrorCode) .
    (eliminate
      LaunchBatchErrorCode
      (lambda unrestricted current : (family LaunchBatchErrorCode) . Bytes)
      code
      (branch LaunchBatchLimitZero . b"ALPHA-HLBT-801")
      (branch LaunchAddressSetEmpty . b"ALPHA-HLBT-802")
      (branch LaunchPayloadRangeWraps . b"ALPHA-HLBT-803")
      (branch LaunchExceedsBatchLimit . b"ALPHA-HLBT-804")
      (branch LaunchPushbufferRejected error . (pushbufferErrorCodeBytes error))))

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

def launchByteLess =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte . (nat-less-than (byte-to-nat left) (byte-to-nat right))))

def launchIf =
  (lambda unrestricted condition : Nat .
    (lambda unrestricted whenTrue : Nat .
      (lambda unrestricted whenFalse : Nat .
        (nat-eliminate
          (lambda unrestricted current : Nat . Nat)
          whenFalse
          (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue))
          condition))))

def launchLexStep =
  (lambda unrestricted left : Byte .
    (lambda unrestricted right : Byte .
      (lambda unrestricted lowerLess : Nat .
        (launchIf
          (launchByteLess left right)
          (succ zero)
          (launchIf (byte-equal left right) lowerLess zero)))))

def launchWord32Less =
  (lambda unrestricted left : (family ModelWord32) .
    (lambda unrestricted right : (family ModelWord32) .
      (eliminate
        ModelWord32
        (lambda unrestricted current : (family ModelWord32) . Nat)
        left
        (branch
          ModelWord32Value
          l0
          l1
          l2
          l3
          .
          (eliminate
            ModelWord32
            (lambda unrestricted current : (family ModelWord32) . Nat)
            right
            (branch
              ModelWord32Value
              r0
              r1
              r2
              r3
              .
              (launchLexStep
                l3
                r3
                (launchLexStep l2 r2 (launchLexStep l1 r1 (launchByteLess l0 r0))))))))))

def launchNaturalWord32 =
  (lambda unrestricted value : Nat .
    (constructor ModelWord32 ModelWord32Value (nat-to-byte value) (byte 0) (byte 0) (byte 0)))

def launchAppendPushbuffer =
  (lambda unrestricted left : (family PushbufferBytesResult) .
    (lambda unrestricted right : (family PushbufferBytesResult) .
      (eliminate
        PushbufferBytesResult
        (lambda unrestricted current : (family PushbufferBytesResult) .
          (family PushbufferBytesResult))
        left
        (branch
          PushbufferBytesReady
          leftBytes
          .
          (eliminate
            PushbufferBytesResult
            (lambda unrestricted current : (family PushbufferBytesResult) .
              (family PushbufferBytesResult))
            right
            (branch
              PushbufferBytesReady
              rightBytes
              .
              (constructor
                PushbufferBytesResult
                PushbufferBytesReady
                (bytes-append leftBytes rightBytes)))
            (branch
              PushbufferBytesRejected
              error
              .
              (constructor PushbufferBytesResult PushbufferBytesRejected error))))
        (branch
          PushbufferBytesRejected
          error
          .
          (constructor PushbufferBytesResult PushbufferBytesRejected error)))))

def launchSynchronization =
  (lambda unrestricted ordering : (family LaunchOrdering) .
    (lambda unrestricted ordinal : Nat .
      (eliminate
        LaunchOrdering
        (lambda unrestricted current : (family LaunchOrdering) . (family PushbufferBytesResult))
        ordering
        (branch LaunchWithIdleBarrier . pushbufferBarrier)
        (branch
          LaunchWithSemaphore
          address
          firstPayload
          .
          (app
            (lambda unrestricted payload : (family ModelWord32) .
              (nat-eliminate
                (lambda unrestricted wrapped : Nat . (family PushbufferBytesResult))
                (launchAppendPushbuffer
                  (pushbufferSemaphoreRelease address payload)
                  (pushbufferSemaphoreAcquire address payload))
                (lambda unrestricted predecessor : Nat .
                  (lambda unrestricted induction : (family PushbufferBytesResult) .
                    (constructor
                      PushbufferBytesResult
                      PushbufferBytesRejected
                      (constructor PushbufferErrorCode PushbufferLengthOutOfRange))))
                (launchWord32Less payload firstPayload)))
            (modelWord32Add firstPayload (launchNaturalWord32 ordinal))))
        (branch LaunchInChannelOrder . (constructor PushbufferBytesResult PushbufferBytesReady b"")))))

def launchEncodeOne =
  (lambda unrestricted ordering : (family LaunchOrdering) .
    (lambda unrestricted ordinal : Nat .
      (lambda unrestricted address : (family ModelWord64) .
        (eliminate
          PushbufferBytesResult
          (lambda unrestricted current : (family PushbufferBytesResult) .
            (family LaunchCommandUnitsResult))
          (launchAppendPushbuffer
            (pushbufferPCASLaunch address)
            (launchSynchronization ordering ordinal))
          (branch
            PushbufferBytesReady
            commandBytes
            .
            (constructor
              LaunchCommandUnitsResult
              LaunchCommandUnitsReady
              (constructor
                LaunchCommandUnits
                LaunchCommandUnitsNext
                (constructor
                  LaunchCommandUnit
                  LaunchCommandUnitValue
                  commandBytes
                  (naturalDivideUnchecked (bytes-length commandBytes) (byte-to-nat (byte 4))))
                (constructor LaunchCommandUnits LaunchCommandUnitsEnd))))
          (branch
            PushbufferBytesRejected
            error
            .
            (constructor
              LaunchCommandUnitsResult
              LaunchCommandUnitsRejected
              (constructor LaunchBatchErrorCode LaunchPushbufferRejected error)))))))

def launchEncodeAddressesWithFuel =
  (lambda unrestricted fuel : Nat .
    (nat-eliminate
      (lambda unrestricted remainingFuel : Nat .
        (pi unrestricted ordering : (family LaunchOrdering) .
          (pi unrestricted ordinal : Nat .
            (pi unrestricted addresses : (family LaunchAddressList) .
              (family LaunchCommandUnitsResult)))))
      (lambda unrestricted ordering : (family LaunchOrdering) .
        (lambda unrestricted ordinal : Nat .
          (lambda unrestricted addresses : (family LaunchAddressList) .
            (constructor
              LaunchCommandUnitsResult
              LaunchCommandUnitsReady
              (constructor LaunchCommandUnits LaunchCommandUnitsEnd)))))
      (lambda unrestricted predecessor : Nat .
        (lambda unrestricted induction : (pi unrestricted ordering : (family LaunchOrdering) . (pi unrestricted ordinal : Nat . (pi unrestricted addresses : (family LaunchAddressList) . (family LaunchCommandUnitsResult)))) .
          (lambda unrestricted ordering : (family LaunchOrdering) .
            (lambda unrestricted ordinal : Nat .
              (lambda unrestricted addresses : (family LaunchAddressList) .
                (eliminate
                  LaunchAddressList
                  (lambda unrestricted current : (family LaunchAddressList) .
                    (family LaunchCommandUnitsResult))
                  addresses
                  (branch
                    LaunchAddressEnd
                    .
                    (constructor
                      LaunchCommandUnitsResult
                      LaunchCommandUnitsReady
                      (constructor LaunchCommandUnits LaunchCommandUnitsEnd)))
                  (branch
                    LaunchAddressNext
                    address
                    tail
                    ih_tail
                    .
                    (eliminate
                      LaunchCommandUnitsResult
                      (lambda unrestricted current : (family LaunchCommandUnitsResult) .
                        (family LaunchCommandUnitsResult))
                      (launchEncodeOne ordering ordinal address)
                      (branch
                        LaunchCommandUnitsReady
                        oneUnits
                        .
                        (eliminate
                          LaunchCommandUnitsResult
                          (lambda unrestricted current : (family LaunchCommandUnitsResult) .
                            (family LaunchCommandUnitsResult))
                          (induction ordering (succ ordinal) tail)
                          (branch
                            LaunchCommandUnitsReady
                            tailUnits
                            .
                            (eliminate
                              LaunchCommandUnits
                              (lambda unrestricted current : (family LaunchCommandUnits) .
                                (family LaunchCommandUnitsResult))
                              oneUnits
                              (branch
                                LaunchCommandUnitsEnd
                                .
                                (constructor
                                  LaunchCommandUnitsResult
                                  LaunchCommandUnitsReady
                                  tailUnits))
                              (branch
                                LaunchCommandUnitsNext
                                unit
                                ignoredTail
                                ih_ignoredTail
                                .
                                (constructor
                                  LaunchCommandUnitsResult
                                  LaunchCommandUnitsReady
                                  (constructor
                                    LaunchCommandUnits
                                    LaunchCommandUnitsNext
                                    unit
                                    tailUnits)))))
                          (branch
                            LaunchCommandUnitsRejected
                            error
                            .
                            (constructor LaunchCommandUnitsResult LaunchCommandUnitsRejected error))))
                      (branch
                        LaunchCommandUnitsRejected
                        error
                        .
                        (constructor LaunchCommandUnitsResult LaunchCommandUnitsRejected error))))))))))
      fuel))

def launchAddressCount =
  (lambda unrestricted addresses : (family LaunchAddressList) .
    (eliminate
      LaunchAddressList
      (lambda unrestricted current : (family LaunchAddressList) . Nat)
      addresses
      (branch LaunchAddressEnd . zero)
      (branch LaunchAddressNext head tail ih_tail . (succ ih_tail))))

def launchPrependUnit =
  (lambda unrestricted maximumDwords : Nat .
    (lambda unrestricted unit : (family LaunchCommandUnit) .
      (lambda unrestricted batches : (family LaunchBatches) .
        (eliminate
          LaunchCommandUnit
          (lambda unrestricted current : (family LaunchCommandUnit) . (family LaunchBatches))
          unit
          (branch
            LaunchCommandUnitValue
            unitBytes
            unitDwords
            .
            (eliminate
              LaunchBatches
              (lambda unrestricted current : (family LaunchBatches) . (family LaunchBatches))
              batches
              (branch
                LaunchBatchesEnd
                .
                (constructor
                  LaunchBatches
                  LaunchBatchesNext
                  (constructor LaunchBatch LaunchBatchValue unitBytes unitDwords)
                  (constructor LaunchBatches LaunchBatchesEnd)))
              (branch
                LaunchBatchesNext
                first
                rest
                ih_rest
                .
                (eliminate
                  LaunchBatch
                  (lambda unrestricted current : (family LaunchBatch) . (family LaunchBatches))
                  first
                  (branch
                    LaunchBatchValue
                    firstBytes
                    firstDwords
                    .
                    (nat-eliminate
                      (lambda unrestricted fits : Nat . (family LaunchBatches))
                      (constructor
                        LaunchBatches
                        LaunchBatchesNext
                        (constructor LaunchBatch LaunchBatchValue unitBytes unitDwords)
                        batches)
                      (lambda unrestricted fitsPredecessor : Nat .
                        (lambda unrestricted fitsInduction : (family LaunchBatches) .
                          (constructor
                            LaunchBatches
                            LaunchBatchesNext
                            (constructor
                              LaunchBatch
                              LaunchBatchValue
                              (bytes-append unitBytes firstBytes)
                              (naturalAdd unitDwords firstDwords))
                            rest)))
                      (naturalLessOrEqual (naturalAdd unitDwords firstDwords) maximumDwords)))))))))))

def launchPackUnits =
  (lambda unrestricted maximumDwords : Nat .
    (lambda unrestricted units : (family LaunchCommandUnits) .
      (eliminate
        LaunchCommandUnits
        (lambda unrestricted current : (family LaunchCommandUnits) . (family LaunchPackResult))
        units
        (branch
          LaunchCommandUnitsEnd
          .
          (constructor
            LaunchPackResult
            LaunchPackReady
            (constructor LaunchBatches LaunchBatchesEnd)))
        (branch
          LaunchCommandUnitsNext
          unit
          tail
          ih_tail
          .
          (eliminate
            LaunchCommandUnit
            (lambda unrestricted current : (family LaunchCommandUnit) . (family LaunchPackResult))
            unit
            (branch
              LaunchCommandUnitValue
              unitBytes
              unitDwords
              .
              (nat-eliminate
                (lambda unrestricted unitFits : Nat . (family LaunchPackResult))
                (constructor
                  LaunchPackResult
                  LaunchPackRejected
                  (constructor LaunchBatchErrorCode LaunchExceedsBatchLimit))
                (lambda unrestricted fitsPredecessor : Nat .
                  (lambda unrestricted fitsInduction : (family LaunchPackResult) .
                    (eliminate
                      LaunchPackResult
                      (lambda unrestricted current : (family LaunchPackResult) .
                        (family LaunchPackResult))
                      ih_tail
                      (branch
                        LaunchPackReady
                        batches
                        .
                        (constructor
                          LaunchPackResult
                          LaunchPackReady
                          (launchPrependUnit maximumDwords unit batches)))
                      (branch
                        LaunchPackRejected
                        error
                        .
                        (constructor LaunchPackResult LaunchPackRejected error)))))
                (naturalLessOrEqual unitDwords maximumDwords))))))))

def launchBatchCount =
  (lambda unrestricted batches : (family LaunchBatches) .
    (eliminate
      LaunchBatches
      (lambda unrestricted current : (family LaunchBatches) . Nat)
      batches
      (branch LaunchBatchesEnd . zero)
      (branch LaunchBatchesNext head tail ih_tail . (succ ih_tail))))

def launchBuildBatchesUnchecked =
  (lambda unrestricted maximumDwords : Nat .
    (lambda unrestricted ordering : (family LaunchOrdering) .
      (lambda unrestricted addresses : (family LaunchAddressList) .
        (nat-eliminate
          (lambda unrestricted maximumPresent : Nat . (family LaunchBatchResult))
          (constructor
            LaunchBatchResult
            LaunchBatchesRejected
            (constructor LaunchBatchErrorCode LaunchBatchLimitZero))
          (lambda unrestricted maximumPredecessor : Nat .
            (lambda unrestricted maximumInduction : (family LaunchBatchResult) .
              (app
                (lambda unrestricted launchCount : Nat .
                  (nat-eliminate
                    (lambda unrestricted launchesPresent : Nat . (family LaunchBatchResult))
                    (constructor
                      LaunchBatchResult
                      LaunchBatchesRejected
                      (constructor LaunchBatchErrorCode LaunchAddressSetEmpty))
                    (lambda unrestricted launchesPredecessor : Nat .
                      (lambda unrestricted launchesInduction : (family LaunchBatchResult) .
                        (eliminate
                          LaunchCommandUnitsResult
                          (lambda unrestricted current : (family LaunchCommandUnitsResult) .
                            (family LaunchBatchResult))
                          (launchEncodeAddressesWithFuel launchCount ordering zero addresses)
                          (branch
                            LaunchCommandUnitsReady
                            units
                            .
                            (eliminate
                              LaunchPackResult
                              (lambda unrestricted current : (family LaunchPackResult) .
                                (family LaunchBatchResult))
                              (launchPackUnits maximumDwords units)
                              (branch
                                LaunchPackReady
                                batches
                                .
                                (constructor
                                  LaunchBatchResult
                                  LaunchBatchesReady
                                  batches
                                  (constructor
                                    LaunchBatchTelemetry
                                    LaunchBatchTelemetryValue
                                    launchCount
                                    (launchBatchCount batches)
                                    zero)))
                              (branch
                                LaunchPackRejected
                                error
                                .
                                (constructor LaunchBatchResult LaunchBatchesRejected error))))
                          (branch
                            LaunchCommandUnitsRejected
                            error
                            .
                            (constructor LaunchBatchResult LaunchBatchesRejected error)))))
                    launchCount))
                (launchAddressCount addresses))))
          maximumDwords))))

def launchOrderingRangeValid =
  (lambda unrestricted ordering : (family LaunchOrdering) .
    (lambda unrestricted launchCount : Nat .
      (eliminate
        LaunchOrdering
        (lambda unrestricted current : (family LaunchOrdering) . Nat)
        ordering
        (branch LaunchWithIdleBarrier . (succ zero))
        (branch
          LaunchWithSemaphore
          address
          firstPayload
          .
          (nat-eliminate
            (lambda unrestricted current : Nat . Nat)
            zero
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : Nat .
                (naturalIsZero
                  (launchWord32Less
                    (modelWord32Add firstPayload (launchNaturalWord32 predecessor))
                    firstPayload))))
            launchCount))
        (branch LaunchInChannelOrder . (succ zero)))))

def launchBuildBatches =
  (lambda unrestricted maximumDwords : Nat .
    (lambda unrestricted ordering : (family LaunchOrdering) .
      (lambda unrestricted addresses : (family LaunchAddressList) .
        (nat-eliminate
          (lambda unrestricted rangeValid : Nat . (family LaunchBatchResult))
          (constructor
            LaunchBatchResult
            LaunchBatchesRejected
            (constructor LaunchBatchErrorCode LaunchPayloadRangeWraps))
          (lambda unrestricted validPredecessor : Nat .
            (lambda unrestricted validInduction : (family LaunchBatchResult) .
              (launchBuildBatchesUnchecked maximumDwords ordering addresses)))
          (launchOrderingRangeValid ordering (launchAddressCount addresses))))))

def launchPhysicalIdentityBindingValid =
  (lambda unrestricted binding : (family LaunchPhysicalIdentityBinding) .
    (eliminate
      LaunchPhysicalIdentityBinding
      (lambda unrestricted current : (family LaunchPhysicalIdentityBinding) . Nat)
      binding
      (branch
        LaunchPhysicalIdentityBindingValue
        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 launchValidatePhysicalReceipt =
  (lambda unrestricted expectedIdentity : Bytes .
    (lambda unrestricted expectedLaunches : Nat .
      (lambda unrestricted receipt : (family LaunchPhysicalReceipt) .
        (eliminate
          LaunchPhysicalReceipt
          (lambda unrestricted current : (family LaunchPhysicalReceipt) .
            (family LaunchPhysicalReceiptResult))
          receipt
          (branch
            LaunchPhysicalReceiptValue
            identity
            binding
            expected
            submitted
            retired
            timestamp
            fallbacks
            .
            (nat-eliminate
              (lambda unrestricted complete : Nat . (family LaunchPhysicalReceiptResult))
              (constructor
                LaunchPhysicalReceiptResult
                LaunchPhysicalReceiptRejected
                (constructor LaunchBatchErrorCode LaunchAddressSetEmpty))
              (lambda unrestricted completePredecessor : Nat .
                (lambda unrestricted completeInduction : (family LaunchPhysicalReceiptResult) .
                  (constructor LaunchPhysicalReceiptResult LaunchPhysicalReceiptAccepted receipt)))
              (naturalAnd
                (naturalEqual (bytes-length expectedIdentity) (byte-to-nat (byte 64)))
                (naturalAnd
                  (bytes-equal expectedIdentity identity)
                  (naturalAnd
                    (launchPhysicalIdentityBindingValid binding)
                    (naturalAnd
                      (naturalEqual expectedLaunches expected)
                      (naturalAnd
                        (naturalEqual expected submitted)
                        (naturalAnd
                          (naturalEqual submitted retired)
                          (naturalAnd
                            (naturalEqual (bytes-length timestamp) (byte-to-nat (byte 8)))
                            (naturalIsZero fallbacks))))))))))))))