module Realization.Nvidia.SM86.ElementwiseVectorSM86

import Accelerator.SM86.Control
import Accelerator.SM86.Immediate
import Accelerator.SM86.Instruction
import Accelerator.SM86.InstructionEncoding
import Accelerator.SM86.Program
import Accelerator.SM86.Types
import Data.SHA256Digest
import Std.Natural
import Std.Byte

family ElementwiseVectorSM86Kind : Type 0
constructor ElementwiseVectorSM86Fill
constructor ElementwiseVectorSM86Copy
constructor ElementwiseVectorSM86Add
constructor ElementwiseVectorSM86Fanout

end-family

family ElementwiseVectorSM86FailureCode : Type 0
constructor ElementwiseVectorSM86ElementCountZero
constructor ElementwiseVectorSM86ElementCountMisaligned
constructor ElementwiseVectorSM86InstructionCountMismatch
constructor ElementwiseVectorSM86EncodingFailed
constructor ElementwiseVectorSM86IdentityInvalid

end-family

family ElementwiseVectorSM86Telemetry : Type 0
constructor ElementwiseVectorSM86TelemetryValue
field unrestricted elementwiseVectorTelemetryKind : (family ElementwiseVectorSM86Kind)
field unrestricted elementwiseVectorTelemetryExpectedInstructions : Nat
field unrestricted elementwiseVectorTelemetryActualInstructions : Nat
field unrestricted elementwiseVectorTelemetryRegisters : Nat
field unrestricted elementwiseVectorTelemetryElements : Nat
field unrestricted elementwiseVectorTelemetryGridX : Nat
field unrestricted elementwiseVectorTelemetryBlockX : Nat
field unrestricted elementwiseVectorTelemetryInputs : Nat
field unrestricted elementwiseVectorTelemetryOutputs : Nat
field unrestricted elementwiseVectorTelemetryScalarBindings : Nat
field unrestricted elementwiseVectorTelemetryHostOperations : Nat
field unrestricted elementwiseVectorTelemetryEncodedBytes : Nat
field unrestricted elementwiseVectorTelemetryEncodedFields : Nat
field unrestricted elementwiseVectorTelemetryEncodedBits : Nat
constructor ElementwiseVectorSM86TelemetryRejected
field unrestricted elementwiseVectorTelemetryFailure : (family ElementwiseVectorSM86FailureCode)
field unrestricted elementwiseVectorTelemetryFailureOrdinal : Nat

end-family

family ElementwiseVectorSM86Plan : Type 0
constructor ElementwiseVectorSM86PlanValue
field unrestricted elementwiseVectorPlanKind : (family ElementwiseVectorSM86Kind)
field unrestricted elementwiseVectorPlanElements : Nat
field unrestricted elementwiseVectorPlanProgram : (family SM86Program)
field unrestricted elementwiseVectorPlanTelemetry : (family ElementwiseVectorSM86Telemetry)

end-family

family ElementwiseVectorSM86PlanResult : Type 0
constructor ElementwiseVectorSM86PlanReady
field unrestricted elementwiseVectorReadyPlan : (family ElementwiseVectorSM86Plan)
constructor ElementwiseVectorSM86PlanFailed
field unrestricted elementwiseVectorPlanFailure : (family ElementwiseVectorSM86FailureCode)
field unrestricted elementwiseVectorPlanFailureTelemetry : (family ElementwiseVectorSM86Telemetry)

end-family

family ElementwiseVectorSM86ImageResult : Type 0
constructor ElementwiseVectorSM86ImageReady
field unrestricted elementwiseVectorImageKind : (family ElementwiseVectorSM86Kind)
field unrestricted elementwiseVectorImageBytes : Bytes
field unrestricted elementwiseVectorImageSHA256 : Bytes
field unrestricted elementwiseVectorImageTelemetry : (family ElementwiseVectorSM86Telemetry)
constructor ElementwiseVectorSM86ImageFailed
field unrestricted elementwiseVectorImageFailure : (family ElementwiseVectorSM86FailureCode)
field unrestricted elementwiseVectorImageFailureInstruction : Nat
field unrestricted elementwiseVectorImageFailureDetail : Bytes
field unrestricted elementwiseVectorImageFailureTelemetry : (family ElementwiseVectorSM86Telemetry)

end-family

def elementwiseVectorNaturalNine =
  (byte-to-nat (byte 9))

def elementwiseVectorNaturalTen =
  (byte-to-nat (byte 10))

def elementwiseVectorNaturalTwelve =
  (byte-to-nat (byte 12))

def elementwiseVectorNaturalThirteen =
  (byte-to-nat (byte 13))

def elementwiseVectorNaturalSixteen =
  (byte-to-nat (byte 16))

def elementwiseVectorNaturalTwentyFour =
  (byte-to-nat (byte 24))

def elementwiseVectorBlockX =
  byteNaturalTwoHundredFiftySix

def elementwiseVectorUnsigned32 =
  (lambda unrestricted b0 : Byte .
    (lambda unrestricted b1 : Byte .
      (lambda unrestricted b2 : Byte .
        (lambda unrestricted b3 : Byte . (sm86Unsigned32 b0 b1 b2 b3)))))

def elementwiseVectorZero =
  (elementwiseVectorUnsigned32 (byte 0) (byte 0) (byte 0) (byte 0))

def elementwiseVectorFour =
  (elementwiseVectorUnsigned32 (byte 4) (byte 0) (byte 0) (byte 0))

def elementwiseVectorTwoHundredFiftySix =
  (elementwiseVectorUnsigned32 (byte 0) (byte 1) (byte 0) (byte 0))

def elementwiseVectorConstantBase =
  (elementwiseVectorUnsigned32 (byte 40) (byte 0) (byte 0) (byte 0))

def elementwiseVectorOutput0 =
  (elementwiseVectorUnsigned32 (byte 96) (byte 1) (byte 0) (byte 0))

def elementwiseVectorInput0 =
  (elementwiseVectorUnsigned32 (byte 104) (byte 1) (byte 0) (byte 0))

def elementwiseVectorInput1OrOutput1 =
  (elementwiseVectorUnsigned32 (byte 112) (byte 1) (byte 0) (byte 0))

def elementwiseVectorScalar0 =
  (elementwiseVectorUnsigned32 (byte 144) (byte 1) (byte 0) (byte 0))

def elementwiseVectorRegister =
  (lambda unrestricted value : Byte . (sm86Register value))

def elementwiseVectorInstruction =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (constructor
      SM86Instruction
      SM86InstructionValue
      (constructor SM86InstructionGuard SM86InstructionAlways)
      body))

def elementwiseVectorNext =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (lambda unrestricted tail : (family SM86Program) .
      (constructor SM86Program SM86ProgramNext (elementwiseVectorInstruction body) tail)))

def elementwiseVectorEnd =
  (constructor SM86Program SM86ProgramEnd)

def elementwiseVectorSet0 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))

def elementwiseVectorSet1 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))

def elementwiseVectorSet2 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))

def elementwiseVectorWait0 =
  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))

def elementwiseVectorWait2 =
  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier2))

def elementwiseVectorWaitSpecials : (family SM86Control) =
  (constructor
    SM86Control
    SM86ControlValue
    (byte 7)
    (constructor SM86YieldMode SM86Continue)
    (constructor SM86Barrier SM86BarrierNone)
    (constructor SM86Barrier SM86BarrierNone)
    (byte 3)
    (byte 0))

def elementwiseVectorWaitInputs : (family SM86Control) =
  (constructor
    SM86Control
    SM86ControlValue
    (byte 7)
    (constructor SM86YieldMode SM86Continue)
    (constructor SM86Barrier SM86BarrierNone)
    (constructor SM86Barrier SM86BarrierNone)
    (byte 3)
    (byte 0))

def elementwiseVectorFillPrologueControl : (family SM86Control) =
  (constructor
    SM86Control
    SM86ControlValue
    (byte 2)
    (constructor SM86YieldMode SM86Yield)
    (constructor SM86Barrier SM86BarrierNone)
    (constructor SM86Barrier SM86BarrierNone)
    (byte 0)
    (byte 0))

def elementwiseVectorFillProgram : (family SM86Program) =
  (elementwiseVectorNext
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      (elementwiseVectorRegister (byte 1))
      (byte 0)
      elementwiseVectorConstantBase
      elementwiseVectorFillPrologueControl)
    (elementwiseVectorNext
      (constructor
        SM86InstructionBody
        SM86SpecialToRegister
        (elementwiseVectorRegister (byte 0))
        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
        elementwiseVectorSet0)
      (elementwiseVectorNext
        (constructor
          SM86InstructionBody
          SM86MoveImmediate
          (elementwiseVectorRegister (byte 3))
          elementwiseVectorFour
          elementwiseVectorWait0)
        (elementwiseVectorNext
          (constructor
            SM86InstructionBody
            SM86SpecialToRegister
            (elementwiseVectorRegister (byte 2))
            (constructor SM86SpecialRegister SM86ThreadIdX)
            elementwiseVectorSet0)
          (elementwiseVectorNext
            (constructor
              SM86InstructionBody
              SM86IntegerMultiplyAddConstant
              (elementwiseVectorRegister (byte 0))
              (elementwiseVectorRegister (byte 0))
              (byte 0)
              elementwiseVectorZero
              (elementwiseVectorRegister (byte 2))
              elementwiseVectorWait0)
            (elementwiseVectorNext
              (constructor
                SM86InstructionBody
                SM86MoveConstant
                (elementwiseVectorRegister (byte 4))
                (byte 0)
                elementwiseVectorScalar0
                sm86SafeControl)
              (elementwiseVectorNext
                (constructor
                  SM86InstructionBody
                  SM86IntegerMultiplyAddWideConstant
                  (elementwiseVectorRegister (byte 6))
                  (elementwiseVectorRegister (byte 0))
                  (elementwiseVectorRegister (byte 3))
                  (byte 0)
                  elementwiseVectorOutput0
                  sm86SafeControl)
                (elementwiseVectorNext
                  (constructor
                    SM86InstructionBody
                    SM86StoreGlobal
                    (elementwiseVectorRegister (byte 6))
                    (elementwiseVectorRegister (byte 4))
                    elementwiseVectorZero
                    sm86SafeControl)
                  (elementwiseVectorNext
                    (constructor SM86InstructionBody SM86Exit sm86BranchControl)
                    elementwiseVectorEnd)))))))))

def elementwiseVectorCopyProgram : (family SM86Program) =
  (elementwiseVectorNext
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      (elementwiseVectorRegister (byte 1))
      (byte 0)
      elementwiseVectorConstantBase
      sm86SafeControl)
    (elementwiseVectorNext
      (constructor
        SM86InstructionBody
        SM86SpecialToRegister
        (elementwiseVectorRegister (byte 0))
        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
        elementwiseVectorSet0)
      (elementwiseVectorNext
        (constructor
          SM86InstructionBody
          SM86SpecialToRegister
          (elementwiseVectorRegister (byte 2))
          (constructor SM86SpecialRegister SM86ThreadIdX)
          elementwiseVectorSet1)
        (elementwiseVectorNext
          (constructor
            SM86InstructionBody
            SM86IntegerMultiplyAddImmediate
            (elementwiseVectorRegister (byte 3))
            (elementwiseVectorRegister (byte 0))
            elementwiseVectorTwoHundredFiftySix
            (elementwiseVectorRegister (byte 2))
            elementwiseVectorWaitSpecials)
          (elementwiseVectorNext
            (constructor
              SM86InstructionBody
              SM86MoveImmediate
              (elementwiseVectorRegister (byte 4))
              elementwiseVectorFour
              sm86SafeControl)
            (elementwiseVectorNext
              (constructor
                SM86InstructionBody
                SM86IntegerMultiplyAddWideConstant
                (elementwiseVectorRegister (byte 6))
                (elementwiseVectorRegister (byte 3))
                (elementwiseVectorRegister (byte 4))
                (byte 0)
                elementwiseVectorInput0
                sm86SafeControl)
              (elementwiseVectorNext
                (constructor
                  SM86InstructionBody
                  SM86LoadGlobal
                  (elementwiseVectorRegister (byte 12))
                  (elementwiseVectorRegister (byte 6))
                  elementwiseVectorZero
                  elementwiseVectorSet2)
                (elementwiseVectorNext
                  (constructor
                    SM86InstructionBody
                    SM86IntegerMultiplyAddWideConstant
                    (elementwiseVectorRegister (byte 8))
                    (elementwiseVectorRegister (byte 3))
                    (elementwiseVectorRegister (byte 4))
                    (byte 0)
                    elementwiseVectorOutput0
                    sm86SafeControl)
                  (elementwiseVectorNext
                    (constructor
                      SM86InstructionBody
                      SM86StoreGlobal
                      (elementwiseVectorRegister (byte 8))
                      (elementwiseVectorRegister (byte 12))
                      elementwiseVectorZero
                      elementwiseVectorWait2)
                    (elementwiseVectorNext
                      (constructor SM86InstructionBody SM86Exit sm86SafeControl)
                      elementwiseVectorEnd))))))))))

def elementwiseVectorAddProgram : (family SM86Program) =
  (elementwiseVectorNext
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      (elementwiseVectorRegister (byte 1))
      (byte 0)
      elementwiseVectorConstantBase
      sm86SafeControl)
    (elementwiseVectorNext
      (constructor
        SM86InstructionBody
        SM86SpecialToRegister
        (elementwiseVectorRegister (byte 0))
        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
        elementwiseVectorSet0)
      (elementwiseVectorNext
        (constructor
          SM86InstructionBody
          SM86SpecialToRegister
          (elementwiseVectorRegister (byte 2))
          (constructor SM86SpecialRegister SM86ThreadIdX)
          elementwiseVectorSet1)
        (elementwiseVectorNext
          (constructor
            SM86InstructionBody
            SM86IntegerMultiplyAddImmediate
            (elementwiseVectorRegister (byte 0))
            (elementwiseVectorRegister (byte 0))
            elementwiseVectorTwoHundredFiftySix
            (elementwiseVectorRegister (byte 2))
            elementwiseVectorWaitSpecials)
          (elementwiseVectorNext
            (constructor
              SM86InstructionBody
              SM86MoveImmediate
              (elementwiseVectorRegister (byte 3))
              elementwiseVectorFour
              sm86SafeControl)
            (elementwiseVectorNext
              (constructor
                SM86InstructionBody
                SM86IntegerMultiplyAddWideConstant
                (elementwiseVectorRegister (byte 6))
                (elementwiseVectorRegister (byte 0))
                (elementwiseVectorRegister (byte 3))
                (byte 0)
                elementwiseVectorInput0
                sm86SafeControl)
              (elementwiseVectorNext
                (constructor
                  SM86InstructionBody
                  SM86LoadGlobal
                  (elementwiseVectorRegister (byte 8))
                  (elementwiseVectorRegister (byte 6))
                  elementwiseVectorZero
                  elementwiseVectorSet0)
                (elementwiseVectorNext
                  (constructor
                    SM86InstructionBody
                    SM86IntegerMultiplyAddWideConstant
                    (elementwiseVectorRegister (byte 10))
                    (elementwiseVectorRegister (byte 0))
                    (elementwiseVectorRegister (byte 3))
                    (byte 0)
                    elementwiseVectorInput1OrOutput1
                    sm86SafeControl)
                  (elementwiseVectorNext
                    (constructor
                      SM86InstructionBody
                      SM86LoadGlobal
                      (elementwiseVectorRegister (byte 12))
                      (elementwiseVectorRegister (byte 10))
                      elementwiseVectorZero
                      elementwiseVectorSet1)
                    (elementwiseVectorNext
                      (constructor
                        SM86InstructionBody
                        SM86IntegerMultiplyAddWideConstant
                        (elementwiseVectorRegister (byte 14))
                        (elementwiseVectorRegister (byte 0))
                        (elementwiseVectorRegister (byte 3))
                        (byte 0)
                        elementwiseVectorOutput0
                        sm86SafeControl)
                      (elementwiseVectorNext
                        (constructor
                          SM86InstructionBody
                          SM86FloatAdd
                          (elementwiseVectorRegister (byte 16))
                          (elementwiseVectorRegister (byte 8))
                          (elementwiseVectorRegister (byte 12))
                          elementwiseVectorWaitInputs)
                        (elementwiseVectorNext
                          (constructor
                            SM86InstructionBody
                            SM86StoreGlobal
                            (elementwiseVectorRegister (byte 14))
                            (elementwiseVectorRegister (byte 16))
                            elementwiseVectorZero
                            sm86SafeControl)
                          (elementwiseVectorNext
                            (constructor SM86InstructionBody SM86Exit sm86SafeControl)
                            elementwiseVectorEnd)))))))))))))

def elementwiseVectorFanoutProgram : (family SM86Program) =
  (elementwiseVectorNext
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      (elementwiseVectorRegister (byte 1))
      (byte 0)
      elementwiseVectorConstantBase
      sm86SafeControl)
    (elementwiseVectorNext
      (constructor
        SM86InstructionBody
        SM86SpecialToRegister
        (elementwiseVectorRegister (byte 0))
        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
        elementwiseVectorSet0)
      (elementwiseVectorNext
        (constructor
          SM86InstructionBody
          SM86SpecialToRegister
          (elementwiseVectorRegister (byte 2))
          (constructor SM86SpecialRegister SM86ThreadIdX)
          elementwiseVectorSet1)
        (elementwiseVectorNext
          (constructor
            SM86InstructionBody
            SM86IntegerMultiplyAddImmediate
            (elementwiseVectorRegister (byte 3))
            (elementwiseVectorRegister (byte 0))
            elementwiseVectorTwoHundredFiftySix
            (elementwiseVectorRegister (byte 2))
            elementwiseVectorWaitSpecials)
          (elementwiseVectorNext
            (constructor
              SM86InstructionBody
              SM86MoveImmediate
              (elementwiseVectorRegister (byte 4))
              elementwiseVectorFour
              sm86SafeControl)
            (elementwiseVectorNext
              (constructor
                SM86InstructionBody
                SM86IntegerMultiplyAddWideConstant
                (elementwiseVectorRegister (byte 6))
                (elementwiseVectorRegister (byte 3))
                (elementwiseVectorRegister (byte 4))
                (byte 0)
                elementwiseVectorInput0
                sm86SafeControl)
              (elementwiseVectorNext
                (constructor
                  SM86InstructionBody
                  SM86LoadGlobal
                  (elementwiseVectorRegister (byte 12))
                  (elementwiseVectorRegister (byte 6))
                  elementwiseVectorZero
                  elementwiseVectorSet2)
                (elementwiseVectorNext
                  (constructor
                    SM86InstructionBody
                    SM86IntegerMultiplyAddWideConstant
                    (elementwiseVectorRegister (byte 8))
                    (elementwiseVectorRegister (byte 3))
                    (elementwiseVectorRegister (byte 4))
                    (byte 0)
                    elementwiseVectorOutput0
                    sm86SafeControl)
                  (elementwiseVectorNext
                    (constructor
                      SM86InstructionBody
                      SM86IntegerMultiplyAddWideConstant
                      (elementwiseVectorRegister (byte 10))
                      (elementwiseVectorRegister (byte 3))
                      (elementwiseVectorRegister (byte 4))
                      (byte 0)
                      elementwiseVectorInput1OrOutput1
                      sm86SafeControl)
                    (elementwiseVectorNext
                      (constructor
                        SM86InstructionBody
                        SM86StoreGlobal
                        (elementwiseVectorRegister (byte 8))
                        (elementwiseVectorRegister (byte 12))
                        elementwiseVectorZero
                        elementwiseVectorWait2)
                      (elementwiseVectorNext
                        (constructor
                          SM86InstructionBody
                          SM86StoreGlobal
                          (elementwiseVectorRegister (byte 10))
                          (elementwiseVectorRegister (byte 12))
                          elementwiseVectorZero
                          sm86SafeControl)
                        (elementwiseVectorNext
                          (constructor SM86InstructionBody SM86Exit sm86SafeControl)
                          elementwiseVectorEnd))))))))))))

def elementwiseVectorProgram =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . (family SM86Program))
      kind
      (branch ElementwiseVectorSM86Fill . elementwiseVectorFillProgram)
      (branch ElementwiseVectorSM86Copy . elementwiseVectorCopyProgram)
      (branch ElementwiseVectorSM86Add . elementwiseVectorAddProgram)
      (branch ElementwiseVectorSM86Fanout . elementwiseVectorFanoutProgram)))

def elementwiseVectorExpectedInstructions =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
      kind
      (branch ElementwiseVectorSM86Fill . elementwiseVectorNaturalNine)
      (branch ElementwiseVectorSM86Copy . elementwiseVectorNaturalTen)
      (branch ElementwiseVectorSM86Add . elementwiseVectorNaturalThirteen)
      (branch ElementwiseVectorSM86Fanout . elementwiseVectorNaturalTwelve)))

def elementwiseVectorRegisterCount =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
      kind
      (branch ElementwiseVectorSM86Fill . elementwiseVectorNaturalSixteen)
      (branch ElementwiseVectorSM86Copy . elementwiseVectorNaturalTwentyFour)
      (branch ElementwiseVectorSM86Add . elementwiseVectorNaturalTwentyFour)
      (branch ElementwiseVectorSM86Fanout . elementwiseVectorNaturalTwentyFour)))

def elementwiseVectorInputCount =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
      kind
      (branch ElementwiseVectorSM86Fill . zero)
      (branch ElementwiseVectorSM86Copy . (succ zero))
      (branch ElementwiseVectorSM86Add . (byte-to-nat (byte 2)))
      (branch ElementwiseVectorSM86Fanout . (succ zero))))

def elementwiseVectorOutputCount =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
      kind
      (branch ElementwiseVectorSM86Fill . (succ zero))
      (branch ElementwiseVectorSM86Copy . (succ zero))
      (branch ElementwiseVectorSM86Add . (succ zero))
      (branch ElementwiseVectorSM86Fanout . (byte-to-nat (byte 2)))))

def elementwiseVectorScalarCount =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (eliminate
      ElementwiseVectorSM86Kind
      (lambda unrestricted current : (family ElementwiseVectorSM86Kind) . Nat)
      kind
      (branch ElementwiseVectorSM86Fill . (succ zero))
      (branch ElementwiseVectorSM86Copy . zero)
      (branch ElementwiseVectorSM86Add . zero)
      (branch ElementwiseVectorSM86Fanout . zero)))

def elementwiseVectorFailureCodeBytes =
  (lambda unrestricted code : (family ElementwiseVectorSM86FailureCode) .
    (eliminate
      ElementwiseVectorSM86FailureCode
      (lambda unrestricted current : (family ElementwiseVectorSM86FailureCode) . Bytes)
      code
      (branch ElementwiseVectorSM86ElementCountZero . b"ALPHA-SM86-VEC-001")
      (branch ElementwiseVectorSM86ElementCountMisaligned . b"ALPHA-SM86-VEC-002")
      (branch ElementwiseVectorSM86InstructionCountMismatch . b"ALPHA-SM86-VEC-003")
      (branch ElementwiseVectorSM86EncodingFailed . b"ALPHA-SM86-VEC-004")
      (branch ElementwiseVectorSM86IdentityInvalid . b"ALPHA-SM86-VEC-005")))

def elementwiseVectorRejectedTelemetry =
  (lambda unrestricted code : (family ElementwiseVectorSM86FailureCode) .
    (lambda unrestricted ordinal : Nat .
      (constructor
        ElementwiseVectorSM86Telemetry
        ElementwiseVectorSM86TelemetryRejected
        code
        ordinal)))

def elementwiseVectorPlan =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (lambda unrestricted elements : Nat .
      (nat-eliminate
        (lambda unrestricted nonzero : Nat . (family ElementwiseVectorSM86PlanResult))
        (constructor
          ElementwiseVectorSM86PlanResult
          ElementwiseVectorSM86PlanFailed
          (constructor ElementwiseVectorSM86FailureCode ElementwiseVectorSM86ElementCountZero)
          (elementwiseVectorRejectedTelemetry
            (constructor ElementwiseVectorSM86FailureCode ElementwiseVectorSM86ElementCountZero)
            zero))
        (lambda unrestricted nonzeroPredecessor : Nat .
          (lambda unrestricted nonzeroInduction : (family ElementwiseVectorSM86PlanResult) .
            (nat-eliminate
              (lambda unrestricted aligned : Nat . (family ElementwiseVectorSM86PlanResult))
              (constructor
                ElementwiseVectorSM86PlanResult
                ElementwiseVectorSM86PlanFailed
                (constructor
                  ElementwiseVectorSM86FailureCode
                  ElementwiseVectorSM86ElementCountMisaligned)
                (elementwiseVectorRejectedTelemetry
                  (constructor
                    ElementwiseVectorSM86FailureCode
                    ElementwiseVectorSM86ElementCountMisaligned)
                  elements))
              (lambda unrestricted alignedPredecessor : Nat .
                (lambda unrestricted alignedInduction : (family ElementwiseVectorSM86PlanResult) .
                  (app
                    (lambda unrestricted program : (family SM86Program) .
                      (app
                        (lambda unrestricted actual : Nat .
                          (nat-eliminate
                            (lambda unrestricted countValid : Nat .
                              (family ElementwiseVectorSM86PlanResult))
                            (constructor
                              ElementwiseVectorSM86PlanResult
                              ElementwiseVectorSM86PlanFailed
                              (constructor
                                ElementwiseVectorSM86FailureCode
                                ElementwiseVectorSM86InstructionCountMismatch)
                              (elementwiseVectorRejectedTelemetry
                                (constructor
                                  ElementwiseVectorSM86FailureCode
                                  ElementwiseVectorSM86InstructionCountMismatch)
                                actual))
                            (lambda unrestricted countPredecessor : Nat .
                              (lambda unrestricted countInduction : (family ElementwiseVectorSM86PlanResult) .
                                (constructor
                                  ElementwiseVectorSM86PlanResult
                                  ElementwiseVectorSM86PlanReady
                                  (constructor
                                    ElementwiseVectorSM86Plan
                                    ElementwiseVectorSM86PlanValue
                                    kind
                                    elements
                                    program
                                    (constructor
                                      ElementwiseVectorSM86Telemetry
                                      ElementwiseVectorSM86TelemetryValue
                                      kind
                                      (elementwiseVectorExpectedInstructions kind)
                                      actual
                                      (elementwiseVectorRegisterCount kind)
                                      elements
                                      (naturalDivideUnchecked elements elementwiseVectorBlockX)
                                      elementwiseVectorBlockX
                                      (elementwiseVectorInputCount kind)
                                      (elementwiseVectorOutputCount kind)
                                      (elementwiseVectorScalarCount kind)
                                      zero
                                      zero
                                      zero
                                      zero)))))
                            (naturalEqual actual (elementwiseVectorExpectedInstructions kind))))
                        (sm86ProgramCount program)))
                    (elementwiseVectorProgram kind))))
              (naturalIsZero (naturalModuloUnchecked elements elementwiseVectorBlockX)))))
        (naturalNonzero elements))))

def elementwiseVectorImage =
  (lambda unrestricted kind : (family ElementwiseVectorSM86Kind) .
    (lambda unrestricted elements : Nat .
      (eliminate
        ElementwiseVectorSM86PlanResult
        (lambda unrestricted current : (family ElementwiseVectorSM86PlanResult) .
          (family ElementwiseVectorSM86ImageResult))
        (elementwiseVectorPlan kind elements)
        (branch
          ElementwiseVectorSM86PlanReady
          plan
          .
          (eliminate
            ElementwiseVectorSM86Plan
            (lambda unrestricted current : (family ElementwiseVectorSM86Plan) .
              (family ElementwiseVectorSM86ImageResult))
            plan
            (branch
              ElementwiseVectorSM86PlanValue
              plannedKind
              plannedElements
              program
              telemetry
              .
              (eliminate
                SM86ProgramEncodingResult
                (lambda unrestricted current : (family SM86ProgramEncodingResult) .
                  (family ElementwiseVectorSM86ImageResult))
                (sm86EncodeProgram program)
                (branch
                  SM86ProgramEncodingSucceeded
                  image
                  encodingTelemetry
                  .
                  (app
                    (lambda unrestricted identity : Bytes .
                      (nat-eliminate
                        (lambda unrestricted valid : Nat .
                          (family ElementwiseVectorSM86ImageResult))
                        (constructor
                          ElementwiseVectorSM86ImageResult
                          ElementwiseVectorSM86ImageFailed
                          (constructor
                            ElementwiseVectorSM86FailureCode
                            ElementwiseVectorSM86IdentityInvalid)
                          zero
                          (elementwiseVectorFailureCodeBytes
                            (constructor
                              ElementwiseVectorSM86FailureCode
                              ElementwiseVectorSM86IdentityInvalid))
                          telemetry)
                        (lambda unrestricted validPredecessor : Nat .
                          (lambda unrestricted validInduction : (family ElementwiseVectorSM86ImageResult) .
                            (eliminate
                              SM86ProgramEncodingTelemetry
                              (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
                                (family ElementwiseVectorSM86ImageResult))
                              encodingTelemetry
                              (branch
                                SM86ProgramEncodingTelemetryValue
                                instructions
                                bytes
                                fields
                                bits
                                highest
                                .
                                (constructor
                                  ElementwiseVectorSM86ImageResult
                                  ElementwiseVectorSM86ImageReady
                                  plannedKind
                                  image
                                  identity
                                  (constructor
                                    ElementwiseVectorSM86Telemetry
                                    ElementwiseVectorSM86TelemetryValue
                                    plannedKind
                                    (elementwiseVectorExpectedInstructions plannedKind)
                                    instructions
                                    (elementwiseVectorRegisterCount plannedKind)
                                    plannedElements
                                    (naturalDivideUnchecked plannedElements elementwiseVectorBlockX)
                                    elementwiseVectorBlockX
                                    (elementwiseVectorInputCount plannedKind)
                                    (elementwiseVectorOutputCount plannedKind)
                                    (elementwiseVectorScalarCount plannedKind)
                                    zero
                                    bytes
                                    fields
                                    bits))))))
                        (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
                    (sha256HexBytesOrEmpty (sha256Hex image))))
                (branch
                  SM86ProgramEncodingFailed
                  index
                  failure
                  encodingTelemetry
                  .
                  (constructor
                    ElementwiseVectorSM86ImageResult
                    ElementwiseVectorSM86ImageFailed
                    (constructor
                      ElementwiseVectorSM86FailureCode
                      ElementwiseVectorSM86EncodingFailed)
                    index
                    (sm86InstructionEncodingStableCode failure)
                    telemetry))))))
        (branch
          ElementwiseVectorSM86PlanFailed
          code
          telemetry
          .
          (constructor
            ElementwiseVectorSM86ImageResult
            ElementwiseVectorSM86ImageFailed
            code
            zero
            (elementwiseVectorFailureCodeBytes code)
            telemetry)))))