836def geluSM86Image =
837 (lambda unrestricted kind : (family GELUSM86ProgramKind) .
838 (lambda unrestricted elements : Nat .
839 (eliminate
840 GELUSM86PlanResult
841 (lambda unrestricted current : (family GELUSM86PlanResult) . (family GELUSM86ImageResult))
842 (geluSM86Plan kind elements)
843 (branch
844 GELUSM86PlanReady
845 plan
846 .
847 (eliminate
848 GELUSM86Plan
849 (lambda unrestricted current : (family GELUSM86Plan) . (family GELUSM86ImageResult))
850 plan
851 (branch
852 GELUSM86PlanValue
853 plannedKind
854 plannedElements
855 program
856 scalars
857 telemetry
858 .
859 (eliminate
860 SM86ProgramEncodingResult
861 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
862 (family GELUSM86ImageResult))
863 (sm86EncodeProgram program)
864 (branch
865 SM86ProgramEncodingSucceeded
866 image
867 encodingTelemetry
868 .
869 (app
870 (lambda unrestricted identity : Bytes .
871 (nat-eliminate
872 (lambda unrestricted valid : Nat . (family GELUSM86ImageResult))
873 (constructor
874 GELUSM86ImageResult
875 GELUSM86ImageFailed
876 (constructor GELUSM86FailureCode GELUSM86IdentityInvalid)
877 zero
878 (geluSM86FailureCodeBytes
879 (constructor GELUSM86FailureCode GELUSM86IdentityInvalid))
880 telemetry)
881 (lambda unrestricted validPredecessor : Nat .
882 (lambda unrestricted validInduction : (family GELUSM86ImageResult) .
883 (eliminate
884 SM86ProgramEncodingTelemetry
885 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
886 (family GELUSM86ImageResult))
887 encodingTelemetry
888 (branch
889 SM86ProgramEncodingTelemetryValue
890 instructions
891 bytes
892 fields
893 bits
894 highest
895 .
896 (constructor
897 GELUSM86ImageResult
898 GELUSM86ImageReady
899 plannedKind
900 image
901 identity
902 (constructor
903 GELUSM86Telemetry
904 GELUSM86TelemetryValue
905 plannedKind
906 (geluSM86ExpectedInstructions plannedKind)
907 instructions
908 (geluSM86RegisterCount plannedKind)
909 plannedElements
910 (naturalDivideUnchecked plannedElements geluSM86BlockX)
911 geluSM86BlockX
912 geluSM86NaturalFive
913 zero
914 bytes
915 fields
916 bits))))))
917 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
918 (sha256HexBytesOrEmpty (sha256Hex image))))
919 (branch
920 SM86ProgramEncodingFailed
921 index
922 failure
923 encodingTelemetry
924 .
925 (constructor
926 GELUSM86ImageResult
927 GELUSM86ImageFailed
928 (constructor GELUSM86FailureCode GELUSM86EncodingFailed)
929 index
930 (sm86InstructionEncodingStableCode failure)
931 telemetry))))))
932 (branch
933 GELUSM86PlanFailed
934 code
935 telemetry
936 .
937 (constructor
938 GELUSM86ImageResult
939 GELUSM86ImageFailed
940 code
941 zero
942 (geluSM86FailureCodeBytes code)
943 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.