Body-digest strategy is now a parameter so the FAST (GPU bring-up) ELF path
can supply a stub instead of paying for a real SHA-256 of the image body.
The digest lives in the image header's telemetry region [112,176); the native
loader jumps straight to the body at offset 176 (NativePhysicalNative.alpha,
"byte 176") and never reads or verifies it, so the choice of digest does not
change what the emitted ELF executes
1109def nativePhysicalGenerateImageWithBodyDigestForFormat =
1110 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1111 (lambda unrestricted digestOfBody : (pi unrestricted bodyInput : Bytes . Bytes) .
1112 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1113 (eliminate
1114 NativePhysicalProgramValidation
1115 (lambda unrestricted current : (family NativePhysicalProgramValidation) .
1116 (family NativePhysicalImageResult))
1117 (nativePhysicalValidateProgram inputProgram)
1118 (branch
1119 NativePhysicalProgramValidated
1120 program
1121 validation
1122 .
1123 (eliminate
1124 NativePhysicalProgram
1125 (lambda unrestricted current : (family NativePhysicalProgram) .
1126 (family NativePhysicalImageResult))
1127 program
1128 (branch
1129 NativePhysicalProgramValue
1130 stateExtent
1131 resultSlots
1132 commands
1133 expected
1134 identity
1135 fallbacks
1136 .
1137 (eliminate
1138 NativePhysicalEncodedCommandsResult
1139 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1140 (family NativePhysicalImageResult))
1141 (nativePhysicalImageEncodeCommandsForFormat format commands)
1142 (branch
1143 NativePhysicalCommandsEncoded
1144 encoded
1145 .
1146 (eliminate
1147 NativePhysicalEncodedCommands
1148 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1149 (family NativePhysicalImageResult))
1150 encoded
1151 (branch
1152 NativePhysicalEncodedCommandsValue
1153 body
1154 commandCount
1155 payloadBytes
1156 auxiliaryBytes
1157 errorBytes
1158 .
1159 (nat-eliminate
1160 (lambda unrestricted current : Nat . (family NativePhysicalImageResult))
1161 (nativePhysicalImageFail
1162 validation
1163 commandCount
1164 (bytes-length body)
1165 (constructor
1166 NativePhysicalImageErrorCode
1167 NativePhysicalImageCommandCountMismatch))
1168 (lambda unrestricted countPredecessor : Nat .
1169 (lambda unrestricted ignoredCount : (family NativePhysicalImageResult) .
1170 (eliminate
1171 NativeTelemetryCounterResult
1172 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1173 (family NativePhysicalImageResult))
1174 (nativeTelemetryCounterFromNatural commandCount)
1175 (branch
1176 NativeTelemetryCounterSucceeded
1177 commandCountWord
1178 .
1179 (eliminate
1180 NativeTelemetryCounterResult
1181 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1182 (family NativePhysicalImageResult))
1183 (nativeTelemetryCounterFromNatural (bytes-length body))
1184 (branch
1185 NativeTelemetryCounterSucceeded
1186 bodyExtent
1187 .
1188 (app
1189 (lambda unrestricted bodyDigest : Bytes .
1190 (app
1191 (lambda unrestricted output : Bytes .
1192 (app
1193 (lambda unrestricted telemetry : (family NativePhysicalImageTelemetry) .
1194 (constructor
1195 NativePhysicalImageResult
1196 NativePhysicalImageGenerated
1197 (constructor
1198 NativePhysicalImage
1199 NativePhysicalImageValue
1200 output
1201 bodyDigest
1202 identity
1203 commandCount
1204 stateExtent
1205 resultSlots
1206 telemetry)
1207 telemetry))
1208 (nativePhysicalImageTelemetryFor
1209 (nativePhysicalCommandsCounts commands)
1210 payloadBytes
1211 auxiliaryBytes
1212 errorBytes
1213 (bytes-length body)
1214 (bytes-length output)
1215 fallbacks
1216 identity
1217 bodyDigest)))
1218 (bytes-append
1219 (nativePhysicalImageMagicFor format)
1220 (bytes-append
1221 (nativePhysicalImageWord64Bytes (nativePhysicalImageVersionFor format))
1222 (bytes-append
1223 (nativePhysicalImageWord64Bytes commandCountWord)
1224 (bytes-append
1225 (nativePhysicalImageWord64Bytes stateExtent)
1226 (bytes-append
1227 (nativePhysicalImageWord64Bytes resultSlots)
1228 (bytes-append
1229 (nativePhysicalImageWord64Bytes bodyExtent)
1230 (bytes-append identity (bytes-append bodyDigest body))))))))))
1231 (digestOfBody body)))
1232 (branch
1233 NativeTelemetryCounterFailed
1234 counterError
1235 naturalValue
1236 .
1237 (nativePhysicalImageFail
1238 validation
1239 commandCount
1240 (bytes-length body)
1241 (constructor
1242 NativePhysicalImageErrorCode
1243 NativePhysicalImageExtentOverflow)))))
1244 (branch
1245 NativeTelemetryCounterFailed
1246 counterError
1247 naturalValue
1248 .
1249 (nativePhysicalImageFail
1250 validation
1251 commandCount
1252 (bytes-length body)
1253 (constructor
1254 NativePhysicalImageErrorCode
1255 NativePhysicalImageExtentOverflow))))))
1256 (naturalEqual commandCount expected)))))
1257 (branch
1258 NativePhysicalCommandsEncodingFailed
1259 error
1260 ordinal
1261 .
1262 (nativePhysicalImageFail validation ordinal zero error))))))
1263 (branch
1264 NativePhysicalProgramRejected
1265 programError
1266 validation
1267 .
1268 (nativePhysicalImageFail
1269 validation
1270 zero
1271 zero
1272 (constructor
1273 NativePhysicalImageErrorCode
1274 NativePhysicalImageProgramRejected
1275 programError)))))))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.