553def embeddingGatherF32ImageFor =
554 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
555 (lambda unrestricted tokenCount : Nat .
556 (eliminate
557 EmbeddingGatherF32PlanResult
558 (lambda unrestricted current : (family EmbeddingGatherF32PlanResult) .
559 (family EmbeddingGatherF32ImageResult))
560 (embeddingGatherF32PlanFor width tokenCount)
561 (branch
562 EmbeddingGatherF32PlanReady
563 plan
564 .
565 (eliminate
566 EmbeddingGatherF32Plan
567 (lambda unrestricted current : (family EmbeddingGatherF32Plan) .
568 (family EmbeddingGatherF32ImageResult))
569 plan
570 (branch
571 EmbeddingGatherF32PlanValue
572 plannedTokens
573 program
574 telemetry
575 .
576 (eliminate
577 SM86ProgramEncodingResult
578 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
579 (family EmbeddingGatherF32ImageResult))
580 (sm86EncodeProgram program)
581 (branch
582 SM86ProgramEncodingSucceeded
583 image
584 encodingTelemetry
585 .
586 (app
587 (lambda unrestricted identity : Bytes .
588 (nat-eliminate
589 (lambda unrestricted identityValid : Nat .
590 (family EmbeddingGatherF32ImageResult))
591 (constructor
592 EmbeddingGatherF32ImageResult
593 EmbeddingGatherF32ImageFailed
594 (constructor
595 EmbeddingGatherF32FailureCode
596 EmbeddingGatherF32IdentityInvalid)
597 zero
598 (embeddingGatherF32FailureCodeBytes
599 (constructor
600 EmbeddingGatherF32FailureCode
601 EmbeddingGatherF32IdentityInvalid))
602 telemetry)
603 (lambda unrestricted identityPredecessor : Nat .
604 (lambda unrestricted identityInduction : (family EmbeddingGatherF32ImageResult) .
605 (eliminate
606 SM86ProgramEncodingTelemetry
607 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
608 (family EmbeddingGatherF32ImageResult))
609 encodingTelemetry
610 (branch
611 SM86ProgramEncodingTelemetryValue
612 instructions
613 bytes
614 fields
615 bits
616 highest
617 .
618 (constructor
619 EmbeddingGatherF32ImageResult
620 EmbeddingGatherF32ImageReady
621 image
622 identity
623 (constructor
624 EmbeddingGatherF32Telemetry
625 EmbeddingGatherF32TelemetryValue
626 embeddingGatherF32NaturalTwenty
627 instructions
628 embeddingGatherF32NaturalTwentyFour
629 plannedTokens
630 plannedTokens
631 (embeddingGatherF32BlockXFor width)
632 (embeddingGatherF32WidthElements width)
633 embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
634 embeddingGatherF32NaturalFour
635 embeddingGatherF32NaturalFour
636 zero
637 bytes
638 fields
639 bits))))))
640 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
641 (sha256HexBytesOrEmpty (sha256Hex image))))
642 (branch
643 SM86ProgramEncodingFailed
644 instructionIndex
645 failure
646 encodingTelemetry
647 .
648 (constructor
649 EmbeddingGatherF32ImageResult
650 EmbeddingGatherF32ImageFailed
651 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32EncodingFailed)
652 instructionIndex
653 (sm86InstructionEncodingStableCode failure)
654 telemetry))))))
655 (branch
656 EmbeddingGatherF32PlanFailed
657 code
658 telemetry
659 .
660 (constructor
661 EmbeddingGatherF32ImageResult
662 EmbeddingGatherF32ImageFailed
663 code
664 zero
665 (embeddingGatherF32FailureCodeBytes code)
666 telemetry)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.