783def indexedRowScatterSM86Build =
784 (lambda unrestricted geometry : (family IndexedRowScatterSM86Geometry) .
785 (app
786 (lambda unrestricted program : (family SM86Program) .
787 (app
788 (lambda unrestricted observedInstructions : Nat .
789 (app
790 (lambda unrestricted manifest : (family IndexedRowScatterSM86Manifest) .
791 (nat-eliminate
792 (lambda unrestricted countMatched : Nat .
793 (family IndexedRowScatterSM86BuildResult))
794 (constructor
795 IndexedRowScatterSM86BuildResult
796 IndexedRowScatterSM86ContractFailed
797 (constructor
798 IndexedRowScatterSM86FailureCode
799 IndexedRowScatterInstructionCountMismatch)
800 (indexedRowScatterSM86TelemetryFor geometry observedInstructions zero))
801 (lambda unrestricted countPredecessor : Nat .
802 (lambda unrestricted countInduction : (family IndexedRowScatterSM86BuildResult) .
803 (app
804 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
805 (eliminate
806 SM86ProgramEncodingResult
807 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
808 (family IndexedRowScatterSM86BuildResult))
809 encoding
810 (branch
811 SM86ProgramEncodingSucceeded
812 bytes
813 encodingTelemetry
814 .
815 (app
816 (lambda unrestricted telemetry : (family IndexedRowScatterSM86Telemetry) .
817 (nat-eliminate
818 (lambda unrestricted bytesMatched : Nat .
819 (family IndexedRowScatterSM86BuildResult))
820 (constructor
821 IndexedRowScatterSM86BuildResult
822 IndexedRowScatterSM86ContractFailed
823 (constructor
824 IndexedRowScatterSM86FailureCode
825 IndexedRowScatterEncodedByteCountMismatch)
826 telemetry)
827 (lambda unrestricted bytesPredecessor : Nat .
828 (lambda unrestricted bytesInduction : (family IndexedRowScatterSM86BuildResult) .
829 (app
830 (lambda unrestricted identityResult : (family SHA256HexResult) .
831 (eliminate
832 SHA256HexResult
833 (lambda unrestricted current : (family SHA256HexResult) .
834 (family IndexedRowScatterSM86BuildResult))
835 identityResult
836 (branch
837 SHA256HexSucceeded
838 identity
839 identityTelemetry
840 .
841 (nat-eliminate
842 (lambda unrestricted identityLengthMatched : Nat .
843 (family IndexedRowScatterSM86BuildResult))
844 (constructor
845 IndexedRowScatterSM86BuildResult
846 IndexedRowScatterSM86ImageIdentityFailed
847 (constructor
848 IndexedRowScatterSM86FailureCode
849 IndexedRowScatterIdentityLengthInvalid)
850 identityResult
851 telemetry)
852 (lambda unrestricted identityLengthPredecessor : Nat .
853 (lambda unrestricted identityLengthInduction : (family IndexedRowScatterSM86BuildResult) .
854 (constructor
855 IndexedRowScatterSM86BuildResult
856 IndexedRowScatterSM86BuildSucceeded
857 bytes
858 identity
859 encodingTelemetry
860 identityTelemetry
861 telemetry)))
862 (naturalEqual
863 (bytes-length identity)
864 indexedRowScatterSM86N64)))
865 (branch
866 SHA256HexFailed
867 error
868 ordinal
869 identityTelemetry
870 .
871 (constructor
872 IndexedRowScatterSM86BuildResult
873 IndexedRowScatterSM86ImageIdentityFailed
874 (constructor
875 IndexedRowScatterSM86FailureCode
876 IndexedRowScatterIdentityFailed)
877 identityResult
878 telemetry))))
879 (sha256Hex bytes))))
880 (naturalEqual
881 (bytes-length bytes)
882 (indexedRowScatterSM86ManifestExpectedBytes manifest))))
883 (indexedRowScatterSM86TelemetryFor
884 geometry
885 observedInstructions
886 (bytes-length bytes))))
887 (branch
888 SM86ProgramEncodingFailed
889 instructionIndex
890 failure
891 encodingTelemetry
892 .
893 (constructor
894 IndexedRowScatterSM86BuildResult
895 IndexedRowScatterSM86ImageEncodingFailed
896 (constructor
897 IndexedRowScatterSM86FailureCode
898 IndexedRowScatterEncodingFailed)
899 encoding
900 (indexedRowScatterSM86TelemetryFor
901 geometry
902 observedInstructions
903 zero)))))
904 (sm86EncodeProgram program))))
905 (naturalEqual
906 observedInstructions
907 (indexedRowScatterSM86ManifestExpectedInstructions manifest))))
908 (indexedRowScatterSM86ManifestFor geometry)))
909 (sm86ProgramCount program)))
910 (indexedRowScatterSM86Program geometry)))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.