955def adamWF32Image =
956 (lambda unrestricted variant : (family AdamWF32SM86Variant) .
957 (lambda unrestricted logicalElements : (family SM86Unsigned32) .
958 (eliminate
959 AdamWF32SM86PlanResult
960 (lambda unrestricted current : (family AdamWF32SM86PlanResult) .
961 (family AdamWF32SM86ImageResult))
962 (adamWF32Plan variant logicalElements)
963 (branch
964 AdamWF32SM86PlanReady
965 plan
966 .
967 (eliminate
968 AdamWF32SM86Plan
969 (lambda unrestricted current : (family AdamWF32SM86Plan) .
970 (family AdamWF32SM86ImageResult))
971 plan
972 (branch
973 AdamWF32SM86PlanValue
974 plannedVariant
975 plannedElements
976 program
977 planTelemetry
978 .
979 (eliminate
980 SM86ProgramEncodingResult
981 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
982 (family AdamWF32SM86ImageResult))
983 (sm86EncodeProgram program)
984 (branch
985 SM86ProgramEncodingSucceeded
986 image
987 encodingTelemetry
988 .
989 (eliminate
990 SM86ProgramEncodingTelemetry
991 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
992 (family AdamWF32SM86ImageResult))
993 encodingTelemetry
994 (branch
995 SM86ProgramEncodingTelemetryValue
996 instructions
997 bytes
998 fields
999 bits
1000 highest
1001 .
1002 (app
1003 (lambda unrestricted telemetry : (family AdamWF32SM86Telemetry) .
1004 (nat-eliminate
1005 (lambda unrestricted byteCountMatched : Nat .
1006 (family AdamWF32SM86ImageResult))
1007 (constructor
1008 AdamWF32SM86ImageResult
1009 AdamWF32SM86ImageFailed
1010 (constructor
1011 AdamWF32SM86FailureCode
1012 AdamWF32SM86EncodedByteCountMismatch)
1013 bytes
1014 (adamWF32SM86FailureCodeBytes
1015 (constructor
1016 AdamWF32SM86FailureCode
1017 AdamWF32SM86EncodedByteCountMismatch))
1018 telemetry)
1019 (lambda unrestricted byteCountPredecessor : Nat .
1020 (lambda unrestricted byteCountInduction : (family AdamWF32SM86ImageResult) .
1021 (eliminate
1022 SHA256HexResult
1023 (lambda unrestricted current : (family SHA256HexResult) .
1024 (family AdamWF32SM86ImageResult))
1025 (sha256Hex image)
1026 (branch
1027 SHA256HexSucceeded
1028 identity
1029 identityTelemetry
1030 .
1031 (nat-eliminate
1032 (lambda unrestricted lengthMatched : Nat .
1033 (family AdamWF32SM86ImageResult))
1034 (constructor
1035 AdamWF32SM86ImageResult
1036 AdamWF32SM86ImageFailed
1037 (constructor
1038 AdamWF32SM86FailureCode
1039 AdamWF32SM86IdentityLengthInvalid)
1040 (bytes-length identity)
1041 (adamWF32SM86FailureCodeBytes
1042 (constructor
1043 AdamWF32SM86FailureCode
1044 AdamWF32SM86IdentityLengthInvalid))
1045 telemetry)
1046 (lambda unrestricted lengthPredecessor : Nat .
1047 (lambda unrestricted lengthInduction : (family AdamWF32SM86ImageResult) .
1048 (constructor
1049 AdamWF32SM86ImageResult
1050 AdamWF32SM86ImageReady
1051 image
1052 identity
1053 encodingTelemetry
1054 identityTelemetry
1055 telemetry)))
1056 (naturalEqual (bytes-length identity) adamWF32N64)))
1057 (branch
1058 SHA256HexFailed
1059 error
1060 ordinal
1061 identityTelemetry
1062 .
1063 (constructor
1064 AdamWF32SM86ImageResult
1065 AdamWF32SM86ImageFailed
1066 (constructor
1067 AdamWF32SM86FailureCode
1068 AdamWF32SM86IdentityFailed)
1069 ordinal
1070 (adamWF32SM86FailureCodeBytes
1071 (constructor
1072 AdamWF32SM86FailureCode
1073 AdamWF32SM86IdentityFailed))
1074 telemetry)))))
1075 (naturalEqual
1076 (bytes-length image)
1077 (adamWF32ExpectedEncodedBytes plannedVariant))))
1078 (adamWF32TelemetryFor
1079 plannedVariant
1080 plannedElements
1081 instructions
1082 bytes
1083 fields
1084 bits
1085 highest
1086 zero)))))
1087 (branch
1088 SM86ProgramEncodingFailed
1089 instructionIndex
1090 failure
1091 encodingTelemetry
1092 .
1093 (constructor
1094 AdamWF32SM86ImageResult
1095 AdamWF32SM86ImageFailed
1096 (constructor AdamWF32SM86FailureCode AdamWF32SM86EncodingFailed)
1097 instructionIndex
1098 (sm86InstructionEncodingStableCode failure)
1099 (adamWF32TelemetryFor
1100 plannedVariant
1101 plannedElements
1102 (sm86ProgramCount program)
1103 zero
1104 zero
1105 zero
1106 zero
1107 instructionIndex)))))))
1108 (branch
1109 AdamWF32SM86PlanFailed
1110 code
1111 telemetry
1112 .
1113 (constructor
1114 AdamWF32SM86ImageResult
1115 AdamWF32SM86ImageFailed
1116 code
1117 zero
1118 (adamWF32SM86FailureCodeBytes code)
1119 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.