1112def nativePhysicalComposePrograms =
1113 (lambda unrestricted training : (family NativePhysicalProgram) .
1114 (lambda unrestricted inference : (family NativePhysicalProgram) .
1115 (lambda unrestricted combinedIdentity : Bytes .
1116 (app
1117 (lambda unrestricted trainingIdentity : Bytes .
1118 (app
1119 (lambda unrestricted inferenceIdentity : Bytes .
1120 (app
1121 (lambda unrestricted trainingCommands :
1122 (family NativePhysicalCommands) .
1123 (app
1124 (lambda unrestricted inferenceCommands :
1125 (family NativePhysicalCommands) .
1126 (nat-eliminate
1127 (lambda unrestricted identityValid : Nat .
1128 (family NativePhysicalProgramComposeResult))
1129 (app
1130 (app
1131 (app
1132 (app
1133 (app
1134 (app
1135 (app
1136 (app
1137 (app
1138 (app
1139 (app
1140 (app nativePhysicalProgramComposeFailure
1141 (constructor NativePhysicalProgramComposeErrorCode
1142 NativePhysicalProgramComposeIdentityInvalid))
1143 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1144 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1145 zero)
1146 zero)
1147 zero)
1148 zero)
1149 zero)
1150 zero)
1151 zero)
1152 trainingIdentity)
1153 inferenceIdentity
1154 combinedIdentity)
1155 (lambda unrestricted identityPredecessor : Nat .
1156 (lambda unrestricted identityInduction :
1157 (family NativePhysicalProgramComposeResult) .
1158 (eliminate NativePhysicalProgramValidation
1159 (lambda unrestricted current :
1160 (family NativePhysicalProgramValidation) .
1161 (family NativePhysicalProgramComposeResult))
1162 (app nativePhysicalValidateProgram training)
1163 (branch NativePhysicalProgramValidated validatedTraining trainingTelemetry .
1164 (eliminate NativePhysicalProgramValidation
1165 (lambda unrestricted current :
1166 (family NativePhysicalProgramValidation) .
1167 (family NativePhysicalProgramComposeResult))
1168 (app nativePhysicalValidateProgram inference)
1169 (branch NativePhysicalProgramValidated validatedInference inferenceTelemetry .
1170 (eliminate NativePhysicalProgram
1171 (lambda unrestricted current :
1172 (family NativePhysicalProgram) .
1173 (family NativePhysicalProgramComposeResult))
1174 training
1175 (branch NativePhysicalProgramValue
1176 trainingState trainingResults ignoredTrainingCommands
1177 trainingExpected ignoredTrainingIdentity trainingFallbacks .
1178 (eliminate NativePhysicalProgram
1179 (lambda unrestricted current :
1180 (family NativePhysicalProgram) .
1181 (family NativePhysicalProgramComposeResult))
1182 inference
1183 (branch NativePhysicalProgramValue
1184 inferenceState inferenceResults ignoredInferenceCommands
1185 inferenceExpected ignoredInferenceIdentity inferenceFallbacks .
1186 (eliminate NativePhysicalProgramComposeStripResult
1187 (lambda unrestricted current :
1188 (family NativePhysicalProgramComposeStripResult) .
1189 (family NativePhysicalProgramComposeResult))
1190 (app nativePhysicalProgramComposeStripTrainingHalt trainingCommands)
1191 (branch NativePhysicalProgramComposeStripEmpty .
1192 (app
1193 (app
1194 (app
1195 (app
1196 (app
1197 (app
1198 (app
1199 (app
1200 (app
1201 (app
1202 (app
1203 (app nativePhysicalProgramComposeFailure
1204 (constructor NativePhysicalProgramComposeErrorCode
1205 NativePhysicalProgramComposeTrainingHaltMissing))
1206 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1207 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1208 zero)
1209 zero)
1210 zero)
1211 zero)
1212 zero)
1213 zero)
1214 (byte-to-nat (byte 2)))
1215 trainingIdentity)
1216 inferenceIdentity
1217 combinedIdentity))
1218 (branch NativePhysicalProgramComposeStripSucceeded
1219 trainingPrefix trainingPrefixCount .
1220 (eliminate ModelWord64CheckedResult
1221 (lambda unrestricted current :
1222 (family ModelWord64CheckedResult) .
1223 (family NativePhysicalProgramComposeResult))
1224 (app nativePhysicalProgramComposeWord64FromNatural
1225 (app nativePhysicalProgramComposeProgramPayloadBytes training))
1226 (branch ModelWord64CheckedSucceeded payloadBase .
1227 (eliminate NativePhysicalProgramComposeCommandsResult
1228 (lambda unrestricted current :
1229 (family NativePhysicalProgramComposeCommandsResult) .
1230 (family NativePhysicalProgramComposeResult))
1231 (app
1232 (app
1233 (app
1234 (app nativePhysicalProgramComposeRelocateCommands inferenceCommands)
1235 trainingState)
1236 trainingResults)
1237 payloadBase)
1238 (branch NativePhysicalProgramComposeCommandsRelocated
1239 relocatedInference commandCount operationCount
1240 operandCount checks .
1241 (eliminate ModelWord64CheckedResult
1242 (lambda unrestricted current :
1243 (family ModelWord64CheckedResult) .
1244 (family NativePhysicalProgramComposeResult))
1245 (app (app modelWord64AddChecked trainingState) inferenceState)
1246 (branch ModelWord64CheckedSucceeded combinedState .
1247 (eliminate ModelWord64CheckedResult
1248 (lambda unrestricted current :
1249 (family ModelWord64CheckedResult) .
1250 (family NativePhysicalProgramComposeResult))
1251 (app (app modelWord64AddChecked trainingResults) inferenceResults)
1252 (branch ModelWord64CheckedSucceeded combinedResults .
1253 (app
1254 (lambda unrestricted combinedCommands :
1255 (family NativePhysicalCommands) .
1256 (app
1257 (lambda unrestricted combinedProgram :
1258 (family NativePhysicalProgram) .
1259 (eliminate NativePhysicalProgramValidation
1260 (lambda unrestricted current :
1261 (family NativePhysicalProgramValidation) .
1262 (family NativePhysicalProgramComposeResult))
1263 (app nativePhysicalValidateProgram combinedProgram)
1264 (branch NativePhysicalProgramValidated validated telemetry .
1265 (constructor NativePhysicalProgramComposeResult
1266 NativePhysicalProgramComposed combinedProgram
1267 (constructor NativePhysicalProgramValidation
1268 NativePhysicalProgramValidated validated telemetry)
1269 (app
1270 (app
1271 (app
1272 (app
1273 (app
1274 (app
1275 (app
1276 (app
1277 (app
1278 (app
1279 (app
1280 (app
1281 (app
1282 (app nativePhysicalProgramComposeTelemetry
1283 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1284 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1285 (app nativePhysicalProgramComposeCommandsCount combinedCommands))
1286 commandCount)
1287 operationCount)
1288 operandCount)
1289 (app (app naturalAdd checks) (succ (succ zero))))
1290 (succ zero))
1291 (byte-to-nat (byte 3)))
1292 zero)
1293 trainingIdentity)
1294 inferenceIdentity)
1295 combinedIdentity)
1296 b"")))
1297 (branch NativePhysicalProgramRejected error telemetry .
1298 (app
1299 (app
1300 (app
1301 (app
1302 (app
1303 (app
1304 (app
1305 (app
1306 (app
1307 (app
1308 (app
1309 (app nativePhysicalProgramComposeFailure
1310 (constructor NativePhysicalProgramComposeErrorCode
1311 NativePhysicalProgramComposeCombinedRejected error))
1312 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1313 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1314 (app nativePhysicalProgramComposeCommandsCount combinedCommands))
1315 commandCount)
1316 operationCount)
1317 operandCount)
1318 (app (app naturalAdd checks) (succ (succ zero))))
1319 (succ zero))
1320 (byte-to-nat (byte 3)))
1321 trainingIdentity)
1322 inferenceIdentity
1323 combinedIdentity))))
1324 (constructor NativePhysicalProgram
1325 NativePhysicalProgramValue
1326 combinedState combinedResults combinedCommands
1327 (app nativePhysicalProgramComposeCommandsCount combinedCommands)
1328 combinedIdentity
1329 (app
1330 (app naturalAdd trainingFallbacks)
1331 inferenceFallbacks))))
1332 (app
1333 (app nativePhysicalProgramComposeCommandsAppend trainingPrefix)
1334 relocatedInference)))
1335 (branch ModelWord64CheckedFailed error .
1336 (app
1337 (app
1338 (app
1339 (app
1340 (app
1341 (app
1342 (app
1343 (app
1344 (app
1345 (app
1346 (app
1347 (app nativePhysicalProgramComposeFailure
1348 (constructor NativePhysicalProgramComposeErrorCode
1349 NativePhysicalProgramComposeArithmeticFailed
1350 (constructor NativePhysicalProgramComposeAddressClass
1351 NativePhysicalProgramComposeResultExtent)
1352 error))
1353 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1354 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1355 zero)
1356 commandCount)
1357 operationCount)
1358 operandCount)
1359 (app (app naturalAdd checks) (succ (succ zero))))
1360 (succ zero))
1361 (byte-to-nat (byte 2)))
1362 trainingIdentity)
1363 inferenceIdentity
1364 combinedIdentity))))
1365 (branch ModelWord64CheckedFailed error .
1366 (app
1367 (app
1368 (app
1369 (app
1370 (app
1371 (app
1372 (app
1373 (app
1374 (app
1375 (app
1376 (app
1377 (app nativePhysicalProgramComposeFailure
1378 (constructor NativePhysicalProgramComposeErrorCode
1379 NativePhysicalProgramComposeArithmeticFailed
1380 (constructor NativePhysicalProgramComposeAddressClass
1381 NativePhysicalProgramComposeStateExtent)
1382 error))
1383 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1384 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1385 zero)
1386 commandCount)
1387 operationCount)
1388 operandCount)
1389 (succ checks))
1390 (succ zero))
1391 (byte-to-nat (byte 2)))
1392 trainingIdentity)
1393 inferenceIdentity
1394 combinedIdentity))))
1395 (branch NativePhysicalProgramComposeCommandsRejected
1396 error commandCount operationCount operandCount checks .
1397 (app
1398 (app
1399 (app
1400 (app
1401 (app
1402 (app
1403 (app
1404 (app
1405 (app
1406 (app
1407 (app
1408 (app nativePhysicalProgramComposeFailure error)
1409 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1410 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1411 zero)
1412 commandCount)
1413 operationCount)
1414 operandCount)
1415 checks)
1416 (succ zero))
1417 (byte-to-nat (byte 2)))
1418 trainingIdentity)
1419 inferenceIdentity
1420 combinedIdentity))))
1421 (branch ModelWord64CheckedFailed error .
1422 (app
1423 (app
1424 (app
1425 (app
1426 (app
1427 (app
1428 (app
1429 (app
1430 (app
1431 (app
1432 (app
1433 (app nativePhysicalProgramComposeFailure
1434 (constructor NativePhysicalProgramComposeErrorCode
1435 NativePhysicalProgramComposeArithmeticFailed
1436 (constructor NativePhysicalProgramComposeAddressClass
1437 NativePhysicalProgramComposePayloadAddress)
1438 error))
1439 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1440 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1441 zero)
1442 zero)
1443 zero)
1444 zero)
1445 zero)
1446 (succ zero))
1447 (byte-to-nat (byte 2)))
1448 trainingIdentity)
1449 inferenceIdentity
1450 combinedIdentity))))
1451 (branch NativePhysicalProgramComposeStripRejected error visited .
1452 (app
1453 (app
1454 (app
1455 (app
1456 (app
1457 (app
1458 (app
1459 (app
1460 (app
1461 (app
1462 (app
1463 (app nativePhysicalProgramComposeFailure error)
1464 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1465 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1466 zero)
1467 zero)
1468 zero)
1469 zero)
1470 zero)
1471 zero)
1472 (byte-to-nat (byte 2)))
1473 trainingIdentity)
1474 inferenceIdentity
1475 combinedIdentity))))))))
1476 (branch NativePhysicalProgramRejected error telemetry .
1477 (app
1478 (app
1479 (app
1480 (app
1481 (app
1482 (app
1483 (app
1484 (app
1485 (app
1486 (app
1487 (app
1488 (app nativePhysicalProgramComposeFailure
1489 (constructor NativePhysicalProgramComposeErrorCode
1490 NativePhysicalProgramComposeInferenceRejected error))
1491 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1492 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1493 zero)
1494 zero)
1495 zero)
1496 zero)
1497 zero)
1498 zero)
1499 (byte-to-nat (byte 2)))
1500 trainingIdentity)
1501 inferenceIdentity
1502 combinedIdentity))))
1503 (branch NativePhysicalProgramRejected error telemetry .
1504 (app
1505 (app
1506 (app
1507 (app
1508 (app
1509 (app
1510 (app
1511 (app
1512 (app
1513 (app
1514 (app
1515 (app nativePhysicalProgramComposeFailure
1516 (constructor NativePhysicalProgramComposeErrorCode
1517 NativePhysicalProgramComposeTrainingRejected error))
1518 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1519 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1520 zero)
1521 zero)
1522 zero)
1523 zero)
1524 zero)
1525 zero)
1526 (succ zero))
1527 trainingIdentity)
1528 inferenceIdentity
1529 combinedIdentity)))))
1530
1531 (app naturalAnd
1532 (app
1533 (app naturalAnd
1534 (app
1535 (app naturalEqual (bytes-length trainingIdentity))
1536 (byte-to-nat (byte 64))))
1537 (app
1538 (app naturalEqual (bytes-length inferenceIdentity))
1539 (byte-to-nat (byte 64))))
1540 (app
1541 (app naturalEqual (bytes-length combinedIdentity))
1542 (byte-to-nat (byte 64))))))
1543 (app nativePhysicalProgramComposeProgramCommands inference)))
1544 (app nativePhysicalProgramComposeProgramCommands training)))
1545 (app nativePhysicalProgramComposeProgramIdentity inference)))
1546 (app nativePhysicalProgramComposeProgramIdentity training)))))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.