module Realization.Nvidia.SM86.AdamWSM86

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

family AdamWF32SM86Variant : Type 0
constructor AdamWF32SM86Unbounded
constructor AdamWF32SM86Bounded

end-family

family AdamWF32SM86FailureCode : Type 0
constructor AdamWF32SM86ElementCountZero
constructor AdamWF32SM86UnboundedExtentMisaligned
constructor AdamWF32SM86InstructionCountMismatch
constructor AdamWF32SM86EncodedByteCountMismatch
constructor AdamWF32SM86EncodingFailed
constructor AdamWF32SM86IdentityFailed
constructor AdamWF32SM86IdentityLengthInvalid

end-family

family AdamWF32SM86ABI : Type 0
constructor AdamWF32SM86ABIValue
field unrestricted adamWF32ABIParameterPointerOffset : Nat
field unrestricted adamWF32ABIGradientPointerOffset : Nat
field unrestricted adamWF32ABIFirstMomentPointerOffset : Nat
field unrestricted adamWF32ABISecondMomentPointerOffset : Nat
field unrestricted adamWF32ABIGradientScaleOffset : Nat
field unrestricted adamWF32ABIBeta1Offset : Nat
field unrestricted adamWF32ABIOneMinusBeta1Offset : Nat
field unrestricted adamWF32ABIBeta2Offset : Nat
field unrestricted adamWF32ABIOneMinusBeta2Offset : Nat
field unrestricted adamWF32ABIDecayMultiplierOffset : Nat
field unrestricted adamWF32ABICorrectedStepSizeOffset : Nat
field unrestricted adamWF32ABIScaledEpsilonOffset : Nat
field unrestricted adamWF32ABIFP32OneOffset : Nat

end-family

family AdamWF32SM86Extents : Type 0
constructor AdamWF32SM86ExtentsValue
field unrestricted adamWF32ExtentsLogicalElements : Nat
field unrestricted adamWF32ExtentsParameterElements : Nat
field unrestricted adamWF32ExtentsGradientElements : Nat
field unrestricted adamWF32ExtentsFirstMomentElements : Nat
field unrestricted adamWF32ExtentsSecondMomentElements : Nat

end-family

family AdamWF32SM86Manifest : Type 0
constructor AdamWF32SM86ManifestValue
field unrestricted adamWF32ManifestVariant : (family AdamWF32SM86Variant)
field unrestricted adamWF32ManifestExpectedInstructions : Nat
field unrestricted adamWF32ManifestExpectedEncodedBytes : Nat
field unrestricted adamWF32ManifestRegisters : Nat
field unrestricted adamWF32ManifestSharedBytes : Nat
field unrestricted adamWF32ManifestGridX : Nat
field unrestricted adamWF32ManifestBlockX : Nat
field unrestricted adamWF32ManifestABI : (family AdamWF32SM86ABI)
field unrestricted adamWF32ManifestExtents : (family AdamWF32SM86Extents)
field unrestricted adamWF32ManifestSetBarrierControls : Nat
field unrestricted adamWF32ManifestWaitSpecialsMask : Nat
field unrestricted adamWF32ManifestWaitLoadsMask : Nat
field unrestricted adamWF32ManifestWaitMufuMask : Nat
field unrestricted adamWF32ManifestGuardedMemoryInstructions : Nat
field unrestricted adamWF32ManifestHostFallbackOperations : Nat

end-family

family AdamWF32SM86Telemetry : Type 0
constructor AdamWF32SM86TelemetryValue
field unrestricted adamWF32TelemetryManifest : (family AdamWF32SM86Manifest)
field unrestricted adamWF32TelemetryObservedInstructions : Nat
field unrestricted adamWF32TelemetryObservedEncodedBytes : Nat
field unrestricted adamWF32TelemetryEncodedFields : Nat
field unrestricted adamWF32TelemetryEncodedBits : Nat
field unrestricted adamWF32TelemetryHighestEncodedBit : Nat
field unrestricted adamWF32TelemetryFailureOrdinal : Nat

end-family

family AdamWF32SM86Plan : Type 0
constructor AdamWF32SM86PlanValue
field unrestricted adamWF32PlanVariant : (family AdamWF32SM86Variant)
field unrestricted adamWF32PlanLogicalElements : Nat
field unrestricted adamWF32PlanProgram : (family SM86Program)
field unrestricted adamWF32PlanTelemetry : (family AdamWF32SM86Telemetry)

end-family

family AdamWF32SM86PlanResult : Type 0
constructor AdamWF32SM86PlanReady
field unrestricted adamWF32ReadyPlan : (family AdamWF32SM86Plan)
constructor AdamWF32SM86PlanFailed
field unrestricted adamWF32PlanFailure : (family AdamWF32SM86FailureCode)
field unrestricted adamWF32PlanFailureTelemetry : (family AdamWF32SM86Telemetry)

end-family

family AdamWF32SM86ImageResult : Type 0
constructor AdamWF32SM86ImageReady
field unrestricted adamWF32ImageBytes : Bytes
field unrestricted adamWF32ImageSHA256 : Bytes
field unrestricted adamWF32ImageEncodingTelemetry : (family SM86ProgramEncodingTelemetry)
field unrestricted adamWF32ImageIdentityTelemetry : (family SHA256DigestTelemetry)
field unrestricted adamWF32ImageTelemetry : (family AdamWF32SM86Telemetry)
constructor AdamWF32SM86ImageFailed
field unrestricted adamWF32ImageFailure : (family AdamWF32SM86FailureCode)
field unrestricted adamWF32ImageFailureOrdinal : Nat
field unrestricted adamWF32ImageFailureDetail : Bytes
field unrestricted adamWF32ImageFailureTelemetry : (family AdamWF32SM86Telemetry)

end-family

def adamWF32SM86FailureCodeBytes =
  (lambda unrestricted code : (family AdamWF32SM86FailureCode) .
    (eliminate
      AdamWF32SM86FailureCode
      (lambda unrestricted current : (family AdamWF32SM86FailureCode) . Bytes)
      code
      (branch AdamWF32SM86ElementCountZero . b"ALPHA-SM86-ADAMW-001")
      (branch AdamWF32SM86UnboundedExtentMisaligned . b"ALPHA-SM86-ADAMW-002")
      (branch AdamWF32SM86InstructionCountMismatch . b"ALPHA-SM86-ADAMW-003")
      (branch AdamWF32SM86EncodedByteCountMismatch . b"ALPHA-SM86-ADAMW-004")
      (branch AdamWF32SM86EncodingFailed . b"ALPHA-SM86-ADAMW-005")
      (branch AdamWF32SM86IdentityFailed . b"ALPHA-SM86-ADAMW-006")
      (branch AdamWF32SM86IdentityLengthInvalid . b"ALPHA-SM86-ADAMW-007")))

def adamWF32R0 =
  (sm86Register (byte 0))

def adamWF32R1 =
  (sm86Register (byte 1))

def adamWF32R2 =
  (sm86Register (byte 2))

def adamWF32R3 =
  (sm86Register (byte 3))

def adamWF32R6 =
  (sm86Register (byte 6))

def adamWF32R8 =
  (sm86Register (byte 8))

def adamWF32R10 =
  (sm86Register (byte 10))

def adamWF32R12 =
  (sm86Register (byte 12))

def adamWF32R14 =
  (sm86Register (byte 14))

def adamWF32R15 =
  (sm86Register (byte 15))

def adamWF32R16 =
  (sm86Register (byte 16))

def adamWF32R17 =
  (sm86Register (byte 17))

def adamWF32R18 =
  (sm86Register (byte 18))

def adamWF32R19 =
  (sm86Register (byte 19))

def adamWF32R20 =
  (sm86Register (byte 20))

def adamWF32R21 =
  (sm86Register (byte 21))

def adamWF32R22 =
  (sm86Register (byte 22))

def adamWF32R23 =
  (sm86Register (byte 23))

def adamWF32R24 =
  (sm86Register (byte 24))

def adamWF32R25 =
  (sm86Register (byte 25))

def adamWF32R26 =
  (sm86Register (byte 26))

def adamWF32R27 =
  (sm86Register (byte 27))

def adamWF32R28 =
  (sm86Register (byte 28))

def adamWF32P0 =
  (constructor SM86Predicate SM86Predicate0)

def adamWF32U0 =
  sm86Unsigned32Zero

def adamWF32U4 =
  (sm86Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))

def adamWF32U256 =
  (sm86Unsigned32 (byte 0) (byte 1) (byte 0) (byte 0))

def adamWF32Offset028 =
  (sm86Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))

def adamWF32Offset160 =
  (sm86Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))

def adamWF32Offset168 =
  (sm86Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))

def adamWF32Offset170 =
  (sm86Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))

def adamWF32Offset178 =
  (sm86Unsigned32 (byte 120) (byte 1) (byte 0) (byte 0))

def adamWF32Offset180 =
  (sm86Unsigned32 (byte 128) (byte 1) (byte 0) (byte 0))

def adamWF32Offset184 =
  (sm86Unsigned32 (byte 132) (byte 1) (byte 0) (byte 0))

def adamWF32Offset188 =
  (sm86Unsigned32 (byte 136) (byte 1) (byte 0) (byte 0))

def adamWF32Offset18c =
  (sm86Unsigned32 (byte 140) (byte 1) (byte 0) (byte 0))

def adamWF32Offset190 =
  (sm86Unsigned32 (byte 144) (byte 1) (byte 0) (byte 0))

def adamWF32Offset194 =
  (sm86Unsigned32 (byte 148) (byte 1) (byte 0) (byte 0))

def adamWF32Offset198 =
  (sm86Unsigned32 (byte 152) (byte 1) (byte 0) (byte 0))

def adamWF32Offset19c =
  (sm86Unsigned32 (byte 156) (byte 1) (byte 0) (byte 0))

def adamWF32Offset1a0 =
  (sm86Unsigned32 (byte 160) (byte 1) (byte 0) (byte 0))

def adamWF32Unsigned32FromNatural =
  (lambda unrestricted value : Nat .
    (app
      (lambda unrestricted quotient1 : Nat .
        (app
          (lambda unrestricted quotient2 : Nat .
            (app
              (lambda unrestricted quotient3 : Nat .
                (sm86Unsigned32
                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
      (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))

def adamWF32Set0 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))

def adamWF32Set1 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))

def adamWF32Set2 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))

def adamWF32Set3 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))

def adamWF32Wait0 =
  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))

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

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

def adamWF32Next =
  (lambda unrestricted body : (family SM86InstructionBody) .
    (lambda unrestricted tail : (family SM86Program) .
      (constructor SM86Program SM86ProgramNext (sm86Instruction body) tail)))

def adamWF32InstructionFor =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted body : (family SM86InstructionBody) .
      (eliminate
        AdamWF32SM86Variant
        (lambda unrestricted current : (family AdamWF32SM86Variant) . (family SM86Instruction))
        variant
        (branch AdamWF32SM86Unbounded . (sm86Instruction body))
        (branch AdamWF32SM86Bounded . (sm86NegatedPredicatedInstruction adamWF32P0 body)))))

def adamWF32GuardedNext =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted body : (family SM86InstructionBody) .
      (lambda unrestricted tail : (family SM86Program) .
        (constructor SM86Program SM86ProgramNext (adamWF32InstructionFor variant body) tail))))

def adamWF32PrefixProgram : (family SM86Program) =
  (adamWF32Next
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      adamWF32R1
      (byte 0)
      adamWF32Offset028
      sm86SafeControl)
    (adamWF32Next
      (constructor
        SM86InstructionBody
        SM86SpecialToRegister
        adamWF32R0
        (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdX)
        adamWF32Set0)
      (adamWF32Next
        (constructor
          SM86InstructionBody
          SM86SpecialToRegister
          adamWF32R2
          (constructor SM86SpecialRegister SM86ThreadIdX)
          adamWF32Set1)
        (adamWF32Next
          (constructor
            SM86InstructionBody
            SM86MoveImmediate
            adamWF32R3
            adamWF32U4
            adamWF32WaitSpecials)
          (adamWF32Next
            (constructor
              SM86InstructionBody
              SM86IntegerMultiplyAddImmediate
              adamWF32R0
              adamWF32R0
              adamWF32U256
              adamWF32R2
              sm86SafeControl)
            (constructor SM86Program SM86ProgramEnd))))))

def adamWF32BoundsProgram =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
      (eliminate
        AdamWF32SM86Variant
        (lambda unrestricted current : (family AdamWF32SM86Variant) . (family SM86Program))
        variant
        (branch AdamWF32SM86Unbounded . (constructor SM86Program SM86ProgramEnd))
        (branch
          AdamWF32SM86Bounded
          .
          (adamWF32Next
            (constructor
              SM86InstructionBody
              SM86PredicateGreaterThanImmediate
              adamWF32P0
              adamWF32R0
              (adamWF32Unsigned32FromNatural
                (naturalPredecessor (sm86Unsigned32Natural logicalElements)))
              sm86SafeControl)
            (constructor SM86Program SM86ProgramEnd))))))

def adamWF32AddressProgram : (family SM86Program) =
  (adamWF32Next
    (constructor
      SM86InstructionBody
      SM86IntegerMultiplyAddWideConstant
      adamWF32R6
      adamWF32R0
      adamWF32R3
      (byte 0)
      adamWF32Offset160
      sm86SafeControl)
    (adamWF32Next
      (constructor
        SM86InstructionBody
        SM86IntegerMultiplyAddWideConstant
        adamWF32R8
        adamWF32R0
        adamWF32R3
        (byte 0)
        adamWF32Offset168
        sm86SafeControl)
      (adamWF32Next
        (constructor
          SM86InstructionBody
          SM86IntegerMultiplyAddWideConstant
          adamWF32R10
          adamWF32R0
          adamWF32R3
          (byte 0)
          adamWF32Offset170
          sm86SafeControl)
        (adamWF32Next
          (constructor
            SM86InstructionBody
            SM86IntegerMultiplyAddWideConstant
            adamWF32R12
            adamWF32R0
            adamWF32R3
            (byte 0)
            adamWF32Offset178
            sm86SafeControl)
          (constructor SM86Program SM86ProgramEnd)))))

def adamWF32LoadProgram =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (adamWF32GuardedNext
      variant
      (constructor
        SM86InstructionBody
        SM86LoadGlobal
        adamWF32R14
        adamWF32R6
        adamWF32U0
        adamWF32Set0)
      (adamWF32GuardedNext
        variant
        (constructor
          SM86InstructionBody
          SM86LoadGlobal
          adamWF32R15
          adamWF32R8
          adamWF32U0
          adamWF32Set1)
        (adamWF32GuardedNext
          variant
          (constructor
            SM86InstructionBody
            SM86LoadGlobal
            adamWF32R16
            adamWF32R10
            adamWF32U0
            adamWF32Set2)
          (adamWF32GuardedNext
            variant
            (constructor
              SM86InstructionBody
              SM86LoadGlobal
              adamWF32R17
              adamWF32R12
              adamWF32U0
              adamWF32Set3)
            (constructor SM86Program SM86ProgramEnd))))))

def adamWF32ScalarProgram : (family SM86Program) =
  (adamWF32Next
    (constructor
      SM86InstructionBody
      SM86MoveConstant
      adamWF32R18
      (byte 0)
      adamWF32Offset180
      sm86SafeControl)
    (adamWF32Next
      (constructor
        SM86InstructionBody
        SM86MoveConstant
        adamWF32R19
        (byte 0)
        adamWF32Offset184
        sm86SafeControl)
      (adamWF32Next
        (constructor
          SM86InstructionBody
          SM86MoveConstant
          adamWF32R20
          (byte 0)
          adamWF32Offset188
          sm86SafeControl)
        (adamWF32Next
          (constructor
            SM86InstructionBody
            SM86MoveConstant
            adamWF32R21
            (byte 0)
            adamWF32Offset18c
            sm86SafeControl)
          (adamWF32Next
            (constructor
              SM86InstructionBody
              SM86MoveConstant
              adamWF32R22
              (byte 0)
              adamWF32Offset190
              sm86SafeControl)
            (adamWF32Next
              (constructor
                SM86InstructionBody
                SM86MoveConstant
                adamWF32R23
                (byte 0)
                adamWF32Offset194
                sm86SafeControl)
              (adamWF32Next
                (constructor
                  SM86InstructionBody
                  SM86MoveConstant
                  adamWF32R24
                  (byte 0)
                  adamWF32Offset198
                  sm86SafeControl)
                (adamWF32Next
                  (constructor
                    SM86InstructionBody
                    SM86MoveConstant
                    adamWF32R25
                    (byte 0)
                    adamWF32Offset19c
                    sm86SafeControl)
                  (constructor SM86Program SM86ProgramEnd)))))))))

def adamWF32MathProgram : (family SM86Program) =
  (adamWF32Next
    (constructor
      SM86InstructionBody
      SM86FloatMultiply
      adamWF32R15
      adamWF32R15
      adamWF32R18
      adamWF32WaitLoads)
    (adamWF32Next
      (constructor
        SM86InstructionBody
        SM86FloatMultiply
        adamWF32R26
        adamWF32R15
        adamWF32R20
        sm86SafeControl)
      (adamWF32Next
        (constructor
          SM86InstructionBody
          SM86FloatFusedMultiplyAdd
          adamWF32R16
          adamWF32R16
          adamWF32R19
          adamWF32R26
          sm86SafeControl)
        (adamWF32Next
          (constructor
            SM86InstructionBody
            SM86FloatMultiply
            adamWF32R28
            adamWF32R15
            adamWF32R15
            sm86SafeControl)
          (adamWF32Next
            (constructor
              SM86InstructionBody
              SM86FloatMultiply
              adamWF32R28
              adamWF32R28
              adamWF32R22
              sm86SafeControl)
            (adamWF32Next
              (constructor
                SM86InstructionBody
                SM86FloatFusedMultiplyAdd
                adamWF32R17
                adamWF32R17
                adamWF32R21
                adamWF32R28
                sm86SafeControl)
              (adamWF32Next
                (constructor
                  SM86InstructionBody
                  SM86MultiFunctionUnitApproximation
                  adamWF32R27
                  adamWF32R17
                  (constructor SM86MultiFunction SM86SquareRoot)
                  adamWF32Set0)
                (adamWF32Next
                  (constructor
                    SM86InstructionBody
                    SM86FloatAdd
                    adamWF32R27
                    adamWF32R27
                    adamWF32R25
                    adamWF32Wait0)
                  (adamWF32Next
                    (constructor
                      SM86InstructionBody
                      SM86MultiFunctionUnitApproximation
                      adamWF32R27
                      adamWF32R27
                      (constructor SM86MultiFunction SM86Reciprocal)
                      adamWF32Set0)
                    (adamWF32Next
                      (constructor
                        SM86InstructionBody
                        SM86FloatMultiply
                        adamWF32R26
                        adamWF32R16
                        adamWF32R24
                        sm86SafeControl)
                      (adamWF32Next
                        (constructor
                          SM86InstructionBody
                          SM86FloatMultiply
                          adamWF32R26
                          adamWF32R26
                          adamWF32R27
                          adamWF32Wait0)
                        (adamWF32Next
                          (constructor
                            SM86InstructionBody
                            SM86FloatNegate
                            adamWF32R26
                            adamWF32R26
                            sm86SafeControl)
                          (adamWF32Next
                            (constructor
                              SM86InstructionBody
                              SM86FloatMultiply
                              adamWF32R14
                              adamWF32R14
                              adamWF32R23
                              sm86SafeControl)
                            (adamWF32Next
                              (constructor
                                SM86InstructionBody
                                SM86FloatAdd
                                adamWF32R14
                                adamWF32R14
                                adamWF32R26
                                sm86SafeControl)
                              (constructor SM86Program SM86ProgramEnd)))))))))))))))

def adamWF32SuffixProgram =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (adamWF32GuardedNext
      variant
      (constructor
        SM86InstructionBody
        SM86StoreGlobal
        adamWF32R6
        adamWF32R14
        adamWF32U0
        sm86SafeControl)
      (adamWF32GuardedNext
        variant
        (constructor
          SM86InstructionBody
          SM86StoreGlobal
          adamWF32R10
          adamWF32R16
          adamWF32U0
          sm86SafeControl)
        (adamWF32GuardedNext
          variant
          (constructor
            SM86InstructionBody
            SM86StoreGlobal
            adamWF32R12
            adamWF32R17
            adamWF32U0
            sm86SafeControl)
          (adamWF32Next
            (constructor SM86InstructionBody SM86Exit sm86SafeControl)
            (constructor SM86Program SM86ProgramEnd))))))

def adamWF32BodyProgram =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (sm86ProgramAppend
      adamWF32AddressProgram
      (sm86ProgramAppend
        (adamWF32LoadProgram variant)
        (sm86ProgramAppend
          adamWF32ScalarProgram
          (sm86ProgramAppend adamWF32MathProgram (adamWF32SuffixProgram variant))))))

def adamWF32ProgramFor =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
      (sm86ProgramAppend
        adamWF32PrefixProgram
        (sm86ProgramAppend
          (adamWF32BoundsProgram variant logicalElements)
          (adamWF32BodyProgram variant)))))

def adamWF32UnboundedProgram : (family SM86Program) =
  (adamWF32ProgramFor (constructor AdamWF32SM86Variant AdamWF32SM86Unbounded) adamWF32U256)

def adamWF32BoundedProgram =
  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
    (adamWF32ProgramFor (constructor AdamWF32SM86Variant AdamWF32SM86Bounded) logicalElements))

def adamWF32N3 =
  (byte-to-nat (byte 3))

def adamWF32N4 =
  (byte-to-nat (byte 4))

def adamWF32N7 =
  (byte-to-nat (byte 7))

def adamWF32N15 =
  (byte-to-nat (byte 15))

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

def adamWF32N32 =
  (byte-to-nat (byte 32))

def adamWF32N39 =
  (byte-to-nat (byte 39))

def adamWF32N40 =
  (byte-to-nat (byte 40))

def adamWF32N64 =
  (byte-to-nat (byte 64))

def adamWF32N255 =
  (byte-to-nat (byte 255))

def adamWF32N256 =
  (succ adamWF32N255)

def adamWF32ExpectedInstructions =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (eliminate
      AdamWF32SM86Variant
      (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
      variant
      (branch AdamWF32SM86Unbounded . adamWF32N39)
      (branch AdamWF32SM86Bounded . adamWF32N40)))

def adamWF32ExpectedEncodedBytes =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (naturalMultiply (adamWF32ExpectedInstructions variant) adamWF32N16))

def adamWF32GridX =
  (lambda unrestricted logicalElements : Nat .
    (naturalDivideUnchecked (naturalAdd logicalElements adamWF32N255) adamWF32N256))

def adamWF32ABI : (family AdamWF32SM86ABI) =
  (constructor
    AdamWF32SM86ABI
    AdamWF32SM86ABIValue
    (sm86Unsigned32Natural adamWF32Offset160)
    (sm86Unsigned32Natural adamWF32Offset168)
    (sm86Unsigned32Natural adamWF32Offset170)
    (sm86Unsigned32Natural adamWF32Offset178)
    (sm86Unsigned32Natural adamWF32Offset180)
    (sm86Unsigned32Natural adamWF32Offset184)
    (sm86Unsigned32Natural adamWF32Offset188)
    (sm86Unsigned32Natural adamWF32Offset18c)
    (sm86Unsigned32Natural adamWF32Offset190)
    (sm86Unsigned32Natural adamWF32Offset194)
    (sm86Unsigned32Natural adamWF32Offset198)
    (sm86Unsigned32Natural adamWF32Offset19c)
    (sm86Unsigned32Natural adamWF32Offset1a0))

-- where the step-dependent scalars sit in the parameter block (a host that
-- supplies them at run time writes there)
def adamWF32CorrectedStepSizeOffsetOf =
  (lambda unrestricted abi : (family AdamWF32SM86ABI) .
    (eliminate AdamWF32SM86ABI (lambda unrestricted current : (family AdamWF32SM86ABI) . Nat) abi
      (branch AdamWF32SM86ABIValue p g m v scale b1 c1 b2 c2 decay step epsilon one . step)))

def adamWF32ScaledEpsilonOffsetOf =
  (lambda unrestricted abi : (family AdamWF32SM86ABI) .
    (eliminate AdamWF32SM86ABI (lambda unrestricted current : (family AdamWF32SM86ABI) . Nat) abi
      (branch AdamWF32SM86ABIValue p g m v scale b1 c1 b2 c2 decay step epsilon one . epsilon)))

def adamWF32GuardedMemoryInstructions =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (eliminate
      AdamWF32SM86Variant
      (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
      variant
      (branch AdamWF32SM86Unbounded . zero)
      (branch AdamWF32SM86Bounded . adamWF32N7)))

def adamWF32ManifestFor =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : Nat .
      (constructor
        AdamWF32SM86Manifest
        AdamWF32SM86ManifestValue
        variant
        (adamWF32ExpectedInstructions variant)
        (adamWF32ExpectedEncodedBytes variant)
        adamWF32N32
        zero
        (adamWF32GridX logicalElements)
        adamWF32N256
        adamWF32ABI
        (constructor
          AdamWF32SM86Extents
          AdamWF32SM86ExtentsValue
          logicalElements
          logicalElements
          logicalElements
          logicalElements
          logicalElements)
        adamWF32N4
        adamWF32N3
        adamWF32N15
        (succ zero)
        (adamWF32GuardedMemoryInstructions variant)
        zero)))

def adamWF32TelemetryFor =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : Nat .
      (lambda unrestricted observedInstructions : Nat .
        (lambda unrestricted observedEncodedBytes : Nat .
          (lambda unrestricted encodedFields : Nat .
            (lambda unrestricted encodedBits : Nat .
              (lambda unrestricted highestEncodedBit : Nat .
                (lambda unrestricted failureOrdinal : Nat .
                  (constructor
                    AdamWF32SM86Telemetry
                    AdamWF32SM86TelemetryValue
                    (adamWF32ManifestFor variant logicalElements)
                    observedInstructions
                    observedEncodedBytes
                    encodedFields
                    encodedBits
                    highestEncodedBit
                    failureOrdinal)))))))))

def adamWF32RejectedTelemetry =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : Nat .
      (lambda unrestricted ordinal : Nat .
        (adamWF32TelemetryFor variant logicalElements zero zero zero zero zero ordinal))))

def adamWF32AlignmentValid =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : Nat .
      (eliminate
        AdamWF32SM86Variant
        (lambda unrestricted current : (family AdamWF32SM86Variant) . Nat)
        variant
        (branch
          AdamWF32SM86Unbounded
          .
          (naturalIsZero (naturalModuloUnchecked logicalElements adamWF32N256)))
        (branch AdamWF32SM86Bounded . (succ zero)))))

def adamWF32Plan =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
      (app
        (lambda unrestricted elements : Nat .
          (nat-eliminate
            (lambda unrestricted nonzero : Nat . (family AdamWF32SM86PlanResult))
            (constructor
              AdamWF32SM86PlanResult
              AdamWF32SM86PlanFailed
              (constructor AdamWF32SM86FailureCode AdamWF32SM86ElementCountZero)
              (adamWF32RejectedTelemetry variant elements zero))
            (lambda unrestricted nonzeroPredecessor : Nat .
              (lambda unrestricted nonzeroInduction : (family AdamWF32SM86PlanResult) .
                (nat-eliminate
                  (lambda unrestricted aligned : Nat . (family AdamWF32SM86PlanResult))
                  (constructor
                    AdamWF32SM86PlanResult
                    AdamWF32SM86PlanFailed
                    (constructor AdamWF32SM86FailureCode AdamWF32SM86UnboundedExtentMisaligned)
                    (adamWF32RejectedTelemetry variant elements elements))
                  (lambda unrestricted alignedPredecessor : Nat .
                    (lambda unrestricted alignedInduction : (family AdamWF32SM86PlanResult) .
                      (app
                        (lambda unrestricted program : (family SM86Program) .
                          (app
                            (lambda unrestricted observedInstructions : Nat .
                              (nat-eliminate
                                (lambda unrestricted countMatched : Nat .
                                  (family AdamWF32SM86PlanResult))
                                (constructor
                                  AdamWF32SM86PlanResult
                                  AdamWF32SM86PlanFailed
                                  (constructor
                                    AdamWF32SM86FailureCode
                                    AdamWF32SM86InstructionCountMismatch)
                                  (adamWF32TelemetryFor
                                    variant
                                    elements
                                    observedInstructions
                                    zero
                                    zero
                                    zero
                                    zero
                                    observedInstructions))
                                (lambda unrestricted countPredecessor : Nat .
                                  (lambda unrestricted countInduction : (family AdamWF32SM86PlanResult) .
                                    (constructor
                                      AdamWF32SM86PlanResult
                                      AdamWF32SM86PlanReady
                                      (constructor
                                        AdamWF32SM86Plan
                                        AdamWF32SM86PlanValue
                                        variant
                                        elements
                                        program
                                        (adamWF32TelemetryFor
                                        variant
                                        elements
                                        observedInstructions
                                        zero
                                        zero
                                        zero
                                        zero
                                        zero)))))
                                (naturalEqual
                                  observedInstructions
                                  (adamWF32ExpectedInstructions variant))))
                            (sm86ProgramCount program)))
                        (adamWF32ProgramFor variant logicalElements))))
                  (adamWF32AlignmentValid variant elements))))
            (naturalNonzero elements)))
        (sm86Unsigned32Natural logicalElements))))

def adamWF32Image =
  (lambda unrestricted variant : (family AdamWF32SM86Variant) .
    (lambda unrestricted logicalElements : (family SM86Unsigned32) .
      (eliminate
        AdamWF32SM86PlanResult
        (lambda unrestricted current : (family AdamWF32SM86PlanResult) .
          (family AdamWF32SM86ImageResult))
        (adamWF32Plan variant logicalElements)
        (branch
          AdamWF32SM86PlanReady
          plan
          .
          (eliminate
            AdamWF32SM86Plan
            (lambda unrestricted current : (family AdamWF32SM86Plan) .
              (family AdamWF32SM86ImageResult))
            plan
            (branch
              AdamWF32SM86PlanValue
              plannedVariant
              plannedElements
              program
              planTelemetry
              .
              (eliminate
                SM86ProgramEncodingResult
                (lambda unrestricted current : (family SM86ProgramEncodingResult) .
                  (family AdamWF32SM86ImageResult))
                (sm86EncodeProgram program)
                (branch
                  SM86ProgramEncodingSucceeded
                  image
                  encodingTelemetry
                  .
                  (eliminate
                    SM86ProgramEncodingTelemetry
                    (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
                      (family AdamWF32SM86ImageResult))
                    encodingTelemetry
                    (branch
                      SM86ProgramEncodingTelemetryValue
                      instructions
                      bytes
                      fields
                      bits
                      highest
                      .
                      (app
                        (lambda unrestricted telemetry : (family AdamWF32SM86Telemetry) .
                          (nat-eliminate
                            (lambda unrestricted byteCountMatched : Nat .
                              (family AdamWF32SM86ImageResult))
                            (constructor
                              AdamWF32SM86ImageResult
                              AdamWF32SM86ImageFailed
                              (constructor
                                AdamWF32SM86FailureCode
                                AdamWF32SM86EncodedByteCountMismatch)
                              bytes
                              (adamWF32SM86FailureCodeBytes
                                (constructor
                                  AdamWF32SM86FailureCode
                                  AdamWF32SM86EncodedByteCountMismatch))
                              telemetry)
                            (lambda unrestricted byteCountPredecessor : Nat .
                              (lambda unrestricted byteCountInduction : (family AdamWF32SM86ImageResult) .
                                (eliminate
                                  SHA256HexResult
                                  (lambda unrestricted current : (family SHA256HexResult) .
                                    (family AdamWF32SM86ImageResult))
                                  (sha256Hex image)
                                  (branch
                                    SHA256HexSucceeded
                                    identity
                                    identityTelemetry
                                    .
                                    (nat-eliminate
                                      (lambda unrestricted lengthMatched : Nat .
                                        (family AdamWF32SM86ImageResult))
                                      (constructor
                                        AdamWF32SM86ImageResult
                                        AdamWF32SM86ImageFailed
                                        (constructor
                                        AdamWF32SM86FailureCode
                                        AdamWF32SM86IdentityLengthInvalid)
                                        (bytes-length identity)
                                        (adamWF32SM86FailureCodeBytes
                                        (constructor
                                        AdamWF32SM86FailureCode
                                        AdamWF32SM86IdentityLengthInvalid))
                                        telemetry)
                                      (lambda unrestricted lengthPredecessor : Nat .
                                        (lambda unrestricted lengthInduction : (family AdamWF32SM86ImageResult) .
                                        (constructor
                                        AdamWF32SM86ImageResult
                                        AdamWF32SM86ImageReady
                                        image
                                        identity
                                        encodingTelemetry
                                        identityTelemetry
                                        telemetry)))
                                      (naturalEqual (bytes-length identity) adamWF32N64)))
                                  (branch
                                    SHA256HexFailed
                                    error
                                    ordinal
                                    identityTelemetry
                                    .
                                    (constructor
                                      AdamWF32SM86ImageResult
                                      AdamWF32SM86ImageFailed
                                      (constructor
                                        AdamWF32SM86FailureCode
                                        AdamWF32SM86IdentityFailed)
                                      ordinal
                                      (adamWF32SM86FailureCodeBytes
                                        (constructor
                                        AdamWF32SM86FailureCode
                                        AdamWF32SM86IdentityFailed))
                                      telemetry)))))
                            (naturalEqual
                              (bytes-length image)
                              (adamWF32ExpectedEncodedBytes plannedVariant))))
                        (adamWF32TelemetryFor
                          plannedVariant
                          plannedElements
                          instructions
                          bytes
                          fields
                          bits
                          highest
                          zero)))))
                (branch
                  SM86ProgramEncodingFailed
                  instructionIndex
                  failure
                  encodingTelemetry
                  .
                  (constructor
                    AdamWF32SM86ImageResult
                    AdamWF32SM86ImageFailed
                    (constructor AdamWF32SM86FailureCode AdamWF32SM86EncodingFailed)
                    instructionIndex
                    (sm86InstructionEncodingStableCode failure)
                    (adamWF32TelemetryFor
                      plannedVariant
                      plannedElements
                      (sm86ProgramCount program)
                      zero
                      zero
                      zero
                      zero
                      instructionIndex)))))))
        (branch
          AdamWF32SM86PlanFailed
          code
          telemetry
          .
          (constructor
            AdamWF32SM86ImageResult
            AdamWF32SM86ImageFailed
            code
            zero
            (adamWF32SM86FailureCodeBytes code)
            telemetry)))))

def adamWF32UnboundedImage =
  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
    (adamWF32Image (constructor AdamWF32SM86Variant AdamWF32SM86Unbounded) logicalElements))

def adamWF32BoundedImage =
  (lambda unrestricted logicalElements : (family SM86Unsigned32) .
    (adamWF32Image (constructor AdamWF32SM86Variant AdamWF32SM86Bounded) logicalElements))