1335def exactCrossEntropySM86Build =
1336 (lambda unrestricted variant : (family ExactCrossEntropySM86Variant) .
1337 (app
1338 (lambda unrestricted program : (family SM86Program) .
1339 (app
1340 (lambda unrestricted observedInstructions : Nat .
1341 (app
1342 (lambda unrestricted manifest : (family ExactCrossEntropySM86Manifest) .
1343 (nat-eliminate
1344 (lambda unrestricted countMatched : Nat .
1345 (family ExactCrossEntropySM86BuildResult))
1346 (constructor
1347 ExactCrossEntropySM86BuildResult
1348 ExactCrossEntropySM86ContractFailed
1349 (constructor
1350 ExactCrossEntropySM86FailureCode
1351 ExactCrossEntropyInstructionCountMismatch)
1352 (exactCrossEntropySM86TelemetryFor variant observedInstructions zero))
1353 (lambda unrestricted countPredecessor : Nat .
1354 (lambda unrestricted countInduction : (family ExactCrossEntropySM86BuildResult) .
1355 (app
1356 (lambda unrestricted encoding : (family SM86ProgramEncodingResult) .
1357 (eliminate
1358 SM86ProgramEncodingResult
1359 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1360 (family ExactCrossEntropySM86BuildResult))
1361 encoding
1362 (branch
1363 SM86ProgramEncodingSucceeded
1364 bytes
1365 encodingTelemetry
1366 .
1367 (app
1368 (lambda unrestricted telemetry : (family ExactCrossEntropySM86Telemetry) .
1369 (nat-eliminate
1370 (lambda unrestricted bytesMatched : Nat .
1371 (family ExactCrossEntropySM86BuildResult))
1372 (constructor
1373 ExactCrossEntropySM86BuildResult
1374 ExactCrossEntropySM86ContractFailed
1375 (constructor
1376 ExactCrossEntropySM86FailureCode
1377 ExactCrossEntropyEncodedByteCountMismatch)
1378 telemetry)
1379 (lambda unrestricted bytesPredecessor : Nat .
1380 (lambda unrestricted bytesInduction : (family ExactCrossEntropySM86BuildResult) .
1381 (app
1382 (lambda unrestricted identityResult : (family SHA256HexResult) .
1383 (eliminate
1384 SHA256HexResult
1385 (lambda unrestricted current : (family SHA256HexResult) .
1386 (family ExactCrossEntropySM86BuildResult))
1387 identityResult
1388 (branch
1389 SHA256HexSucceeded
1390 identity
1391 identityTelemetry
1392 .
1393 (nat-eliminate
1394 (lambda unrestricted identityLengthMatched : Nat .
1395 (family ExactCrossEntropySM86BuildResult))
1396 (constructor
1397 ExactCrossEntropySM86BuildResult
1398 ExactCrossEntropySM86ImageIdentityFailed
1399 (constructor
1400 ExactCrossEntropySM86FailureCode
1401 ExactCrossEntropyIdentityLengthInvalid)
1402 identityResult
1403 telemetry)
1404 (lambda unrestricted identityLengthPredecessor : Nat .
1405 (lambda unrestricted identityLengthInduction : (family ExactCrossEntropySM86BuildResult) .
1406 (constructor
1407 ExactCrossEntropySM86BuildResult
1408 ExactCrossEntropySM86BuildSucceeded
1409 bytes
1410 identity
1411 encodingTelemetry
1412 identityTelemetry
1413 telemetry)))
1414 (naturalEqual
1415 (bytes-length identity)
1416 exactCrossEntropySM86N64)))
1417 (branch
1418 SHA256HexFailed
1419 error
1420 ordinal
1421 identityTelemetry
1422 .
1423 (constructor
1424 ExactCrossEntropySM86BuildResult
1425 ExactCrossEntropySM86ImageIdentityFailed
1426 (constructor
1427 ExactCrossEntropySM86FailureCode
1428 ExactCrossEntropyIdentityFailed)
1429 identityResult
1430 telemetry))))
1431 (sha256Hex bytes))))
1432 (naturalEqual
1433 (bytes-length bytes)
1434 (exactCrossEntropySM86ManifestBytes manifest))))
1435 (exactCrossEntropySM86TelemetryFor
1436 variant
1437 observedInstructions
1438 (bytes-length bytes))))
1439 (branch
1440 SM86ProgramEncodingFailed
1441 instructionIndex
1442 failure
1443 encodingTelemetry
1444 .
1445 (constructor
1446 ExactCrossEntropySM86BuildResult
1447 ExactCrossEntropySM86ImageEncodingFailed
1448 (constructor
1449 ExactCrossEntropySM86FailureCode
1450 ExactCrossEntropyEncodingFailed)
1451 encoding
1452 (exactCrossEntropySM86TelemetryFor
1453 variant
1454 observedInstructions
1455 zero)))))
1456 (sm86EncodeProgram program))))
1457 (naturalEqual
1458 observedInstructions
1459 (exactCrossEntropySM86ManifestInstructions manifest))))
1460 (exactCrossEntropySM86ManifestFor variant)))
1461 (sm86ProgramCount program)))
1462 (exactCrossEntropySM86ProgramFor variant)))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.