588def exactCrossEntropyBackwardBuild =
589 (app
590 (lambda unrestricted observedInstructions : Nat .
591 (nat-eliminate
592 (lambda unrestricted countMatched : Nat . (family ExactCrossEntropyBackwardSM86BuildResult))
593 (constructor
594 ExactCrossEntropyBackwardSM86BuildResult
595 ExactCrossEntropyBackwardSM86ContractFailed
596 (constructor
597 ExactCrossEntropyBackwardSM86FailureCode
598 ExactCrossEntropyBackwardInstructionCountMismatch)
599 (exactCrossEntropyBackwardTelemetryFor observedInstructions zero))
600 (lambda unrestricted countPredecessor : Nat .
601 (lambda unrestricted countInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
602 (app
603 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
604 (eliminate
605 SM86ProgramEncodingResult
606 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
607 (family ExactCrossEntropyBackwardSM86BuildResult))
608 encoding
609 (branch
610 SM86ProgramEncodingSucceeded
611 bytes
612 encodingTelemetry
613 .
614 (app
615 (lambda unrestricted telemetry : (family ExactCrossEntropyBackwardSM86Telemetry) .
616 (nat-eliminate
617 (lambda unrestricted bytesMatched : Nat .
618 (family ExactCrossEntropyBackwardSM86BuildResult))
619 (constructor
620 ExactCrossEntropyBackwardSM86BuildResult
621 ExactCrossEntropyBackwardSM86ContractFailed
622 (constructor
623 ExactCrossEntropyBackwardSM86FailureCode
624 ExactCrossEntropyBackwardEncodedByteCountMismatch)
625 telemetry)
626 (lambda unrestricted bytesPredecessor : Nat .
627 (lambda unrestricted bytesInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
628 (app
629 (lambda unrestricted identityResult : (family SHA256HexResult) .
630 (eliminate
631 SHA256HexResult
632 (lambda unrestricted current : (family SHA256HexResult) .
633 (family ExactCrossEntropyBackwardSM86BuildResult))
634 identityResult
635 (branch
636 SHA256HexSucceeded
637 identity
638 identityTelemetry
639 .
640 (nat-eliminate
641 (lambda unrestricted identityLengthMatched : Nat .
642 (family ExactCrossEntropyBackwardSM86BuildResult))
643 (constructor
644 ExactCrossEntropyBackwardSM86BuildResult
645 ExactCrossEntropyBackwardSM86ImageIdentityFailed
646 (constructor
647 ExactCrossEntropyBackwardSM86FailureCode
648 ExactCrossEntropyBackwardIdentityLengthInvalid)
649 identityResult
650 telemetry)
651 (lambda unrestricted identityLengthPredecessor : Nat .
652 (lambda unrestricted identityLengthInduction : (family ExactCrossEntropyBackwardSM86BuildResult) .
653 (constructor
654 ExactCrossEntropyBackwardSM86BuildResult
655 ExactCrossEntropyBackwardSM86BuildSucceeded
656 bytes
657 identity
658 encodingTelemetry
659 identityTelemetry
660 telemetry)))
661 (naturalEqual (bytes-length identity) 64)))
662 (branch
663 SHA256HexFailed
664 error
665 ordinal
666 identityTelemetry
667 .
668 (constructor
669 ExactCrossEntropyBackwardSM86BuildResult
670 ExactCrossEntropyBackwardSM86ImageIdentityFailed
671 (constructor
672 ExactCrossEntropyBackwardSM86FailureCode
673 ExactCrossEntropyBackwardIdentityFailed)
674 identityResult
675 telemetry))))
676 (sha256Hex bytes))))
677 (naturalEqual
678 (bytes-length bytes)
679 (exactCrossEntropyBackwardManifestBytes
680 exactCrossEntropyBackwardManifest))))
681 (exactCrossEntropyBackwardTelemetryFor
682 observedInstructions
683 (bytes-length bytes))))
684 (branch
685 SM86ProgramEncodingFailed
686 instructionIndex
687 failure
688 encodingTelemetry
689 .
690 (constructor
691 ExactCrossEntropyBackwardSM86BuildResult
692 ExactCrossEntropyBackwardSM86ImageEncodingFailed
693 (constructor
694 ExactCrossEntropyBackwardSM86FailureCode
695 ExactCrossEntropyBackwardEncodingFailed)
696 encoding
697 (exactCrossEntropyBackwardTelemetryFor observedInstructions zero)))))
698 (sm86EncodeProgram exactCrossEntropyBackwardProgram))))
699 (naturalEqual
700 observedInstructions
701 (exactCrossEntropyBackwardManifestInstructions exactCrossEntropyBackwardManifest))))
702 (sm86ProgramCount exactCrossEntropyBackwardProgram))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.