562def embeddingGatherF32ImageFor =
563 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
564 (lambda unrestricted tokenCount : Nat .
565 (eliminate
566 EmbeddingGatherF32PlanResult
567 (lambda unrestricted current : (family EmbeddingGatherF32PlanResult) .
568 (family EmbeddingGatherF32ImageResult))
569 (embeddingGatherF32PlanFor width tokenCount)
570 (branch
571 EmbeddingGatherF32PlanReady
572 plan
573 .
574 (eliminate
575 EmbeddingGatherF32Plan
576 (lambda unrestricted current : (family EmbeddingGatherF32Plan) .
577 (family EmbeddingGatherF32ImageResult))
578 plan
579 (branch
580 EmbeddingGatherF32PlanValue
581 plannedTokens
582 program
583 telemetry
584 .
585 (eliminate
586 SM86ProgramEncodingResult
587 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
588 (family EmbeddingGatherF32ImageResult))
589 (sm86EncodeProgram program)
590 (branch
591 SM86ProgramEncodingSucceeded
592 image
593 encodingTelemetry
594 .
595 (app
596 (lambda unrestricted identity : Bytes .
597 (nat-eliminate
598 (lambda unrestricted identityValid : Nat .
599 (family EmbeddingGatherF32ImageResult))
600 (constructor
601 EmbeddingGatherF32ImageResult
602 EmbeddingGatherF32ImageFailed
603 (constructor
604 EmbeddingGatherF32FailureCode
605 EmbeddingGatherF32IdentityInvalid)
606 zero
607 (embeddingGatherF32FailureCodeBytes
608 (constructor
609 EmbeddingGatherF32FailureCode
610 EmbeddingGatherF32IdentityInvalid))
611 telemetry)
612 (lambda unrestricted identityPredecessor : Nat .
613 (lambda unrestricted identityInduction : (family EmbeddingGatherF32ImageResult) .
614 (eliminate
615 SM86ProgramEncodingTelemetry
616 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
617 (family EmbeddingGatherF32ImageResult))
618 encodingTelemetry
619 (branch
620 SM86ProgramEncodingTelemetryValue
621 instructions
622 bytes
623 fields
624 bits
625 highest
626 .
627 (constructor
628 EmbeddingGatherF32ImageResult
629 EmbeddingGatherF32ImageReady
630 image
631 identity
632 (constructor
633 EmbeddingGatherF32Telemetry
634 EmbeddingGatherF32TelemetryValue
635 embeddingGatherF32NaturalTwenty
636 instructions
637 embeddingGatherF32NaturalTwentyFour
638 plannedTokens
639 plannedTokens
640 (embeddingGatherF32BlockXFor width)
641 (embeddingGatherF32WidthElements width)
642 embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
643 embeddingGatherF32NaturalFour
644 embeddingGatherF32NaturalFour
645 zero
646 bytes
647 fields
648 bits))))))
649 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
650 (sha256HexBytesOrEmpty (sha256Hex image))))
651 (branch
652 SM86ProgramEncodingFailed
653 instructionIndex
654 failure
655 encodingTelemetry
656 .
657 (constructor
658 EmbeddingGatherF32ImageResult
659 EmbeddingGatherF32ImageFailed
660 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32EncodingFailed)
661 instructionIndex
662 (sm86InstructionEncodingStableCode failure)
663 telemetry))))))
664 (branch
665 EmbeddingGatherF32PlanFailed
666 code
667 telemetry
668 .
669 (constructor
670 EmbeddingGatherF32ImageResult
671 EmbeddingGatherF32ImageFailed
672 code
673 zero
674 (embeddingGatherF32FailureCodeBytes code)
675 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.