module Realization.Nvidia.SM86.EmbeddingGatherF32SM86

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 EmbeddingGatherF32FailureCode : Type 0
constructor EmbeddingGatherF32TokenOutOfBounds
constructor EmbeddingGatherF32ChannelOutOfBounds
constructor EmbeddingGatherF32TokenCountZero
constructor EmbeddingGatherF32InstructionCountMismatch
constructor EmbeddingGatherF32EncodingFailed
constructor EmbeddingGatherF32IdentityInvalid

end-family

family EmbeddingGatherF32OffsetResult : Type 0
constructor EmbeddingGatherF32OffsetValid
field unrestricted embeddingGatherF32OffsetBytes : Nat
constructor EmbeddingGatherF32OffsetInvalid
field unrestricted embeddingGatherF32OffsetFailure : (family EmbeddingGatherF32FailureCode)
field unrestricted embeddingGatherF32RejectedToken : Nat
field unrestricted embeddingGatherF32RejectedChannel : Nat

end-family

family EmbeddingGatherF32Telemetry : Type 0
constructor EmbeddingGatherF32TelemetryValue
field unrestricted embeddingGatherF32TelemetryExpectedInstructions : Nat
field unrestricted embeddingGatherF32TelemetryActualInstructions : Nat
field unrestricted embeddingGatherF32TelemetryRegisterCount : Nat
field unrestricted embeddingGatherF32TelemetryTokenCount : Nat
field unrestricted embeddingGatherF32TelemetryGridY : Nat
field unrestricted embeddingGatherF32TelemetryBlockX : Nat
field unrestricted embeddingGatherF32TelemetryWidth : Nat
field unrestricted embeddingGatherF32TelemetryVocabulary : Nat
field unrestricted embeddingGatherF32TelemetryScalarLoads : Nat
field unrestricted embeddingGatherF32TelemetryScalarStores : Nat
field unrestricted embeddingGatherF32TelemetryHostOperations : Nat
field unrestricted embeddingGatherF32TelemetryEncodedBytes : Nat
field unrestricted embeddingGatherF32TelemetryEncodedFields : Nat
field unrestricted embeddingGatherF32TelemetryEncodedBits : Nat
constructor EmbeddingGatherF32TelemetryRejected
field unrestricted embeddingGatherF32TelemetryFailure : (family EmbeddingGatherF32FailureCode)
field unrestricted embeddingGatherF32TelemetryFailureOrdinal : Nat

end-family

family EmbeddingGatherF32Plan : Type 0
constructor EmbeddingGatherF32PlanValue
field unrestricted embeddingGatherF32PlanTokenCount : Nat
field unrestricted embeddingGatherF32PlanProgram : (family SM86Program)
field unrestricted embeddingGatherF32PlanTelemetry : (family EmbeddingGatherF32Telemetry)

end-family

family EmbeddingGatherF32PlanResult : Type 0
constructor EmbeddingGatherF32PlanReady
field unrestricted embeddingGatherF32ReadyPlan : (family EmbeddingGatherF32Plan)
constructor EmbeddingGatherF32PlanFailed
field unrestricted embeddingGatherF32PlanFailure : (family EmbeddingGatherF32FailureCode)
field unrestricted embeddingGatherF32PlanFailureTelemetry : (family EmbeddingGatherF32Telemetry)

end-family

family EmbeddingGatherF32ImageResult : Type 0
constructor EmbeddingGatherF32ImageReady
field unrestricted embeddingGatherF32ImageBytes : Bytes
field unrestricted embeddingGatherF32ImageSHA256 : Bytes
field unrestricted embeddingGatherF32ImageTelemetry : (family EmbeddingGatherF32Telemetry)
constructor EmbeddingGatherF32ImageFailed
field unrestricted embeddingGatherF32ImageFailure : (family EmbeddingGatherF32FailureCode)
field unrestricted embeddingGatherF32ImageFailureInstruction : Nat
field unrestricted embeddingGatherF32ImageFailureCode : Bytes
field unrestricted embeddingGatherF32ImageFailureTelemetry : (family EmbeddingGatherF32Telemetry)

end-family

-- Each thread moves four floats. A width choice determines both the row
-- stride in the program and the number of threads in its launch.
family EmbeddingGatherF32Width : Type 0
constructor EmbeddingGatherF32Width1024
constructor EmbeddingGatherF32Width576
constructor EmbeddingGatherF32Width512
constructor EmbeddingGatherF32Width256

end-family

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

def embeddingGatherF32NaturalTwenty =
  (byte-to-nat (byte 20))

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

def embeddingGatherF32NaturalOneThousandTwentyFour =
  (naturalMultiply (byte-to-nat (byte 4)) byteNaturalTwoHundredFiftySix)

def embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight =
  (naturalMultiply (byte-to-nat (byte 48)) byteNaturalTwoHundredFiftySix)

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

def embeddingGatherF32Unsigned32 =
  (lambda unrestricted byte0 : Byte .
    (lambda unrestricted byte1 : Byte .
      (lambda unrestricted byte2 : Byte .
        (lambda unrestricted byte3 : Byte . (sm86Unsigned32 byte0 byte1 byte2 byte3)))))

def embeddingGatherF32ZeroImmediate =
  (embeddingGatherF32Unsigned32 (byte 0) (byte 0) (byte 0) (byte 0))

def embeddingGatherF32FourImmediate =
  (embeddingGatherF32Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))

def embeddingGatherF32EightImmediate =
  (embeddingGatherF32Unsigned32 (byte 8) (byte 0) (byte 0) (byte 0))

def embeddingGatherF32TwelveImmediate =
  (embeddingGatherF32Unsigned32 (byte 12) (byte 0) (byte 0) (byte 0))

def embeddingGatherF32WidthElements =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (eliminate
      EmbeddingGatherF32Width
      (lambda unrestricted current : (family EmbeddingGatherF32Width) . Nat)
      width
      (branch EmbeddingGatherF32Width1024 . embeddingGatherF32NaturalOneThousandTwentyFour)
      (branch EmbeddingGatherF32Width576 .
        (naturalAdd
          (naturalMultiply (byte-to-nat (byte 2)) byteNaturalTwoHundredFiftySix)
          (byte-to-nat (byte 64))))
      (branch
        EmbeddingGatherF32Width512
        .
        (naturalAdd byteNaturalTwoHundredFiftySix byteNaturalTwoHundredFiftySix))
      (branch EmbeddingGatherF32Width256 . byteNaturalTwoHundredFiftySix)))

-- The family above bounds every width to a 32-bit immediate. Keeping this
-- conversion tied to the row width prevents launch and address drift.
def embeddingGatherF32WidthImmediateFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (sm86Unsigned32FromNaturalTruncated (embeddingGatherF32WidthElements width)))

def embeddingGatherF32BlockXFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (naturalDivideUnchecked
      (embeddingGatherF32WidthElements width)
      embeddingGatherF32NaturalFour))

def embeddingGatherF32ConstantBase =
  (embeddingGatherF32Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))

-- CB0 pointer ordinal contract for the gather's output, token stream and
-- F32 embedding table. The launch planner turns these into QMD-relative
-- parameter patches; system code never repeats their word offsets.
def embeddingGatherF32OutputArgument : Nat = 0
def embeddingGatherF32TokenIdsArgument : Nat = 1
def embeddingGatherF32EmbeddingArgument : Nat = 2
def embeddingGatherF32ArgumentCount : Nat = 3

def embeddingGatherF32OutputPointer =
  (embeddingGatherF32Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))

def embeddingGatherF32TokenIdsPointer =
  (embeddingGatherF32Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))

def embeddingGatherF32EmbeddingPointer =
  (embeddingGatherF32Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))

def embeddingGatherF32SetBarrier0 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))

def embeddingGatherF32SetBarrier1 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))

def embeddingGatherF32SetBarrier2 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))

def embeddingGatherF32SetBarrier3 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))

def embeddingGatherF32SetBarrier4 =
  (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier4))

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

def embeddingGatherF32WaitToken =
  (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))

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

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

def embeddingGatherF32Append =
  (lambda unrestricted left : (family SM86Program) .
    (lambda unrestricted right : (family SM86Program) . (sm86ProgramAppend left right)))

def embeddingGatherF32Prologue =
  (embeddingGatherF32Append
    (embeddingGatherF32Instruction
      (constructor
        SM86InstructionBody
        SM86MoveConstant
        (embeddingGatherF32Register (byte 1))
        (byte 0)
        embeddingGatherF32ConstantBase
        sm86SafeControl))
    (embeddingGatherF32Append
      (embeddingGatherF32Instruction
        (constructor
          SM86InstructionBody
          SM86SpecialToRegister
          (embeddingGatherF32Register (byte 0))
          (constructor SM86SpecialRegister SM86ThreadIdX)
          embeddingGatherF32SetBarrier0))
      (embeddingGatherF32Append
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86SpecialToRegister
            (embeddingGatherF32Register (byte 4))
            (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY)
            embeddingGatherF32SetBarrier1))
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86MoveImmediate
            (embeddingGatherF32Register (byte 3))
            embeddingGatherF32FourImmediate
            embeddingGatherF32WaitSpecials)))))

def embeddingGatherF32AddressProgramFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (embeddingGatherF32Append
      (embeddingGatherF32Instruction
        (constructor
          SM86InstructionBody
          SM86IntegerMultiplyAddImmediate
          (embeddingGatherF32Register (byte 6))
          (embeddingGatherF32Register (byte 0))
          embeddingGatherF32FourImmediate
          sm86ZeroRegister
          sm86SafeControl))
      (embeddingGatherF32Append
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86IntegerMultiplyAddWideConstant
            (embeddingGatherF32Register (byte 8))
            (embeddingGatherF32Register (byte 4))
            (embeddingGatherF32Register (byte 3))
            (byte 0)
            embeddingGatherF32TokenIdsPointer
            sm86SafeControl))
        (embeddingGatherF32Append
          (embeddingGatherF32Instruction
            (constructor
              SM86InstructionBody
              SM86LoadGlobal
              (embeddingGatherF32Register (byte 10))
              (embeddingGatherF32Register (byte 8))
              embeddingGatherF32ZeroImmediate
              embeddingGatherF32SetBarrier0))
          (embeddingGatherF32Append
            (embeddingGatherF32Instruction
              (constructor
                SM86InstructionBody
                SM86IntegerMultiplyAddImmediate
                (embeddingGatherF32Register (byte 18))
                (embeddingGatherF32Register (byte 4))
                (embeddingGatherF32WidthImmediateFor width)
                (embeddingGatherF32Register (byte 6))
                sm86SafeControl))
            (embeddingGatherF32Append
              (embeddingGatherF32Instruction
                (constructor
                  SM86InstructionBody
                  SM86IntegerMultiplyAddWideConstant
                  (embeddingGatherF32Register (byte 20))
                  (embeddingGatherF32Register (byte 18))
                  (embeddingGatherF32Register (byte 3))
                  (byte 0)
                  embeddingGatherF32OutputPointer
                  sm86SafeControl))
              (embeddingGatherF32Append
                (embeddingGatherF32Instruction
                  (constructor
                    SM86InstructionBody
                    SM86IntegerMultiplyAddImmediate
                    (embeddingGatherF32Register (byte 12))
                    (embeddingGatherF32Register (byte 10))
                    (embeddingGatherF32WidthImmediateFor width)
                    (embeddingGatherF32Register (byte 6))
                    embeddingGatherF32WaitToken))
                (embeddingGatherF32Instruction
                  (constructor
                    SM86InstructionBody
                    SM86IntegerMultiplyAddWideConstant
                    (embeddingGatherF32Register (byte 14))
                    (embeddingGatherF32Register (byte 12))
                    (embeddingGatherF32Register (byte 3))
                    (byte 0)
                    embeddingGatherF32EmbeddingPointer
                    sm86SafeControl)))))))))

def embeddingGatherF32AddressProgram =
  (embeddingGatherF32AddressProgramFor
    (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024))

def embeddingGatherF32Loads =
  (embeddingGatherF32Append
    (embeddingGatherF32Instruction
      (constructor
        SM86InstructionBody
        SM86LoadGlobal
        (embeddingGatherF32Register (byte 16))
        (embeddingGatherF32Register (byte 14))
        embeddingGatherF32ZeroImmediate
        embeddingGatherF32SetBarrier1))
    (embeddingGatherF32Append
      (embeddingGatherF32Instruction
        (constructor
          SM86InstructionBody
          SM86LoadGlobal
          (embeddingGatherF32Register (byte 17))
          (embeddingGatherF32Register (byte 14))
          embeddingGatherF32FourImmediate
          embeddingGatherF32SetBarrier2))
      (embeddingGatherF32Append
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86LoadGlobal
            (embeddingGatherF32Register (byte 18))
            (embeddingGatherF32Register (byte 14))
            embeddingGatherF32EightImmediate
            embeddingGatherF32SetBarrier3))
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86LoadGlobal
            (embeddingGatherF32Register (byte 19))
            (embeddingGatherF32Register (byte 14))
            embeddingGatherF32TwelveImmediate
            embeddingGatherF32SetBarrier4)))))

def embeddingGatherF32Stores =
  (embeddingGatherF32Append
    (embeddingGatherF32Instruction
      (constructor
        SM86InstructionBody
        SM86StoreGlobal
        (embeddingGatherF32Register (byte 20))
        (embeddingGatherF32Register (byte 16))
        embeddingGatherF32ZeroImmediate
        embeddingGatherF32WaitEmbedding))
    (embeddingGatherF32Append
      (embeddingGatherF32Instruction
        (constructor
          SM86InstructionBody
          SM86StoreGlobal
          (embeddingGatherF32Register (byte 20))
          (embeddingGatherF32Register (byte 17))
          embeddingGatherF32FourImmediate
          sm86SafeControl))
      (embeddingGatherF32Append
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86StoreGlobal
            (embeddingGatherF32Register (byte 20))
            (embeddingGatherF32Register (byte 18))
            embeddingGatherF32EightImmediate
            sm86SafeControl))
        (embeddingGatherF32Instruction
          (constructor
            SM86InstructionBody
            SM86StoreGlobal
            (embeddingGatherF32Register (byte 20))
            (embeddingGatherF32Register (byte 19))
            embeddingGatherF32TwelveImmediate
            sm86SafeControl)))))

def embeddingGatherF32Exit =
  (embeddingGatherF32Instruction (constructor SM86InstructionBody SM86Exit sm86SafeControl))

def embeddingGatherF32ProgramFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (embeddingGatherF32Append
      embeddingGatherF32Prologue
      (embeddingGatherF32Append
        (embeddingGatherF32AddressProgramFor width)
        (embeddingGatherF32Append
          embeddingGatherF32Loads
          (embeddingGatherF32Append embeddingGatherF32Stores embeddingGatherF32Exit)))))

def embeddingGatherF32Program : (family SM86Program) =
  (embeddingGatherF32ProgramFor (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024))

def embeddingGatherF32FailureCodeBytes =
  (lambda unrestricted code : (family EmbeddingGatherF32FailureCode) .
    (eliminate
      EmbeddingGatherF32FailureCode
      (lambda unrestricted current : (family EmbeddingGatherF32FailureCode) . Bytes)
      code
      (branch EmbeddingGatherF32TokenOutOfBounds . b"ALPHA-SM86-EMB-001")
      (branch EmbeddingGatherF32ChannelOutOfBounds . b"ALPHA-SM86-EMB-002")
      (branch EmbeddingGatherF32TokenCountZero . b"ALPHA-SM86-EMB-003")
      (branch EmbeddingGatherF32InstructionCountMismatch . b"ALPHA-SM86-EMB-004")
      (branch EmbeddingGatherF32EncodingFailed . b"ALPHA-SM86-EMB-005")
      (branch EmbeddingGatherF32IdentityInvalid . b"ALPHA-SM86-EMB-006")))

def embeddingGatherF32Offset =
  (lambda unrestricted token : Nat .
    (lambda unrestricted channel : Nat .
      (nat-eliminate
        (lambda unrestricted tokenValid : Nat . (family EmbeddingGatherF32OffsetResult))
        (constructor
          EmbeddingGatherF32OffsetResult
          EmbeddingGatherF32OffsetInvalid
          (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenOutOfBounds)
          token
          channel)
        (lambda unrestricted tokenPredecessor : Nat .
          (lambda unrestricted tokenInduction : (family EmbeddingGatherF32OffsetResult) .
            (nat-eliminate
              (lambda unrestricted channelValid : Nat . (family EmbeddingGatherF32OffsetResult))
              (constructor
                EmbeddingGatherF32OffsetResult
                EmbeddingGatherF32OffsetInvalid
                (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32ChannelOutOfBounds)
                token
                channel)
              (lambda unrestricted channelPredecessor : Nat .
                (lambda unrestricted channelInduction : (family EmbeddingGatherF32OffsetResult) .
                  (constructor
                    EmbeddingGatherF32OffsetResult
                    EmbeddingGatherF32OffsetValid
                    (naturalMultiply
                      embeddingGatherF32NaturalFour
                      (naturalAdd
                        (naturalMultiply token embeddingGatherF32NaturalOneThousandTwentyFour)
                        channel)))))
              (naturalLess channel embeddingGatherF32NaturalOneThousandTwentyFour))))
        (naturalLess token embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight))))

def embeddingGatherF32RejectedTelemetry =
  (lambda unrestricted code : (family EmbeddingGatherF32FailureCode) .
    (lambda unrestricted ordinal : Nat .
      (constructor EmbeddingGatherF32Telemetry EmbeddingGatherF32TelemetryRejected code ordinal)))

def embeddingGatherF32PlanFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (lambda unrestricted tokenCount : Nat .
      (nat-eliminate
        (lambda unrestricted tokenCountNonzero : Nat . (family EmbeddingGatherF32PlanResult))
        (constructor
          EmbeddingGatherF32PlanResult
          EmbeddingGatherF32PlanFailed
          (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
          (embeddingGatherF32RejectedTelemetry
            (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
            zero))
        (lambda unrestricted nonzeroPredecessor : Nat .
          (lambda unrestricted nonzeroInduction : (family EmbeddingGatherF32PlanResult) .
            (app
              (lambda unrestricted actualInstructions : Nat .
                (nat-eliminate
                  (lambda unrestricted countValid : Nat . (family EmbeddingGatherF32PlanResult))
                  (constructor
                    EmbeddingGatherF32PlanResult
                    EmbeddingGatherF32PlanFailed
                    (constructor
                      EmbeddingGatherF32FailureCode
                      EmbeddingGatherF32InstructionCountMismatch)
                    (embeddingGatherF32RejectedTelemetry
                      (constructor
                        EmbeddingGatherF32FailureCode
                        EmbeddingGatherF32InstructionCountMismatch)
                      actualInstructions))
                  (lambda unrestricted countPredecessor : Nat .
                    (lambda unrestricted countInduction : (family EmbeddingGatherF32PlanResult) .
                      (constructor
                        EmbeddingGatherF32PlanResult
                        EmbeddingGatherF32PlanReady
                        (constructor
                          EmbeddingGatherF32Plan
                          EmbeddingGatherF32PlanValue
                          tokenCount
                          (embeddingGatherF32ProgramFor width)
                          (constructor
                            EmbeddingGatherF32Telemetry
                            EmbeddingGatherF32TelemetryValue
                            embeddingGatherF32NaturalTwenty
                            actualInstructions
                            embeddingGatherF32NaturalTwentyFour
                            tokenCount
                            tokenCount
                            (embeddingGatherF32BlockXFor width)
                            (embeddingGatherF32WidthElements width)
                            embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
                            embeddingGatherF32NaturalFour
                            embeddingGatherF32NaturalFour
                            zero
                            zero
                            zero
                            zero)))))
                  (naturalEqual actualInstructions embeddingGatherF32NaturalTwenty)))
              (sm86ProgramCount (embeddingGatherF32ProgramFor width)))))
        (naturalNonzero tokenCount))))

def embeddingGatherF32Plan =
  (lambda unrestricted tokenCount : Nat .
    (embeddingGatherF32PlanFor
      (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024)
      tokenCount))

def embeddingGatherF32ImageFor =
  (lambda unrestricted width : (family EmbeddingGatherF32Width) .
    (lambda unrestricted tokenCount : Nat .
      (eliminate
        EmbeddingGatherF32PlanResult
        (lambda unrestricted current : (family EmbeddingGatherF32PlanResult) .
          (family EmbeddingGatherF32ImageResult))
        (embeddingGatherF32PlanFor width tokenCount)
        (branch
          EmbeddingGatherF32PlanReady
          plan
          .
          (eliminate
            EmbeddingGatherF32Plan
            (lambda unrestricted current : (family EmbeddingGatherF32Plan) .
              (family EmbeddingGatherF32ImageResult))
            plan
            (branch
              EmbeddingGatherF32PlanValue
              plannedTokens
              program
              telemetry
              .
              (eliminate
                SM86ProgramEncodingResult
                (lambda unrestricted current : (family SM86ProgramEncodingResult) .
                  (family EmbeddingGatherF32ImageResult))
                (sm86EncodeProgram program)
                (branch
                  SM86ProgramEncodingSucceeded
                  image
                  encodingTelemetry
                  .
                  (app
                    (lambda unrestricted identity : Bytes .
                      (nat-eliminate
                        (lambda unrestricted identityValid : Nat .
                          (family EmbeddingGatherF32ImageResult))
                        (constructor
                          EmbeddingGatherF32ImageResult
                          EmbeddingGatherF32ImageFailed
                          (constructor
                            EmbeddingGatherF32FailureCode
                            EmbeddingGatherF32IdentityInvalid)
                          zero
                          (embeddingGatherF32FailureCodeBytes
                            (constructor
                              EmbeddingGatherF32FailureCode
                              EmbeddingGatherF32IdentityInvalid))
                          telemetry)
                        (lambda unrestricted identityPredecessor : Nat .
                          (lambda unrestricted identityInduction : (family EmbeddingGatherF32ImageResult) .
                            (eliminate
                              SM86ProgramEncodingTelemetry
                              (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
                                (family EmbeddingGatherF32ImageResult))
                              encodingTelemetry
                              (branch
                                SM86ProgramEncodingTelemetryValue
                                instructions
                                bytes
                                fields
                                bits
                                highest
                                .
                                (constructor
                                  EmbeddingGatherF32ImageResult
                                  EmbeddingGatherF32ImageReady
                                  image
                                  identity
                                  (constructor
                                    EmbeddingGatherF32Telemetry
                                    EmbeddingGatherF32TelemetryValue
                                    embeddingGatherF32NaturalTwenty
                                    instructions
                                    embeddingGatherF32NaturalTwentyFour
                                    plannedTokens
                                    plannedTokens
                                    (embeddingGatherF32BlockXFor width)
                                    (embeddingGatherF32WidthElements width)
                                    embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
                                    embeddingGatherF32NaturalFour
                                    embeddingGatherF32NaturalFour
                                    zero
                                    bytes
                                    fields
                                    bits))))))
                        (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
                    (sha256HexBytesOrEmpty (sha256Hex image))))
                (branch
                  SM86ProgramEncodingFailed
                  instructionIndex
                  failure
                  encodingTelemetry
                  .
                  (constructor
                    EmbeddingGatherF32ImageResult
                    EmbeddingGatherF32ImageFailed
                    (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32EncodingFailed)
                    instructionIndex
                    (sm86InstructionEncodingStableCode failure)
                    telemetry))))))
        (branch
          EmbeddingGatherF32PlanFailed
          code
          telemetry
          .
          (constructor
            EmbeddingGatherF32ImageResult
            EmbeddingGatherF32ImageFailed
            code
            zero
            (embeddingGatherF32FailureCodeBytes code)
            telemetry)))))

def embeddingGatherF32Image =
  (lambda unrestricted tokenCount : Nat .
    (embeddingGatherF32ImageFor
      (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024)
      tokenCount))