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
1492def nativePhysicalGenerateImageWithBodyDigestForFormat =
1493 (lambda unrestricted format : (family NativePhysicalImageFormat) .
1494 (lambda unrestricted digestOfBody : (pi unrestricted bodyInput : Bytes . Bytes) .
1495 (lambda unrestricted inputProgram : (family NativePhysicalProgram) .
1496 (eliminate
1497 NativePhysicalProgramValidation
1498 (lambda unrestricted current : (family NativePhysicalProgramValidation) .
1499 (family NativePhysicalImageResult))
1500 (nativePhysicalValidateProgram inputProgram)
1501 (branch
1502 NativePhysicalProgramValidated
1503 program
1504 validation
1505 .
1506 (eliminate
1507 NativePhysicalProgram
1508 (lambda unrestricted current : (family NativePhysicalProgram) .
1509 (family NativePhysicalImageResult))
1510 program
1511 (branch
1512 NativePhysicalProgramValue
1513 stateExtent
1514 resultSlots
1515 commands
1516 expected
1517 identity
1518 fallbacks
1519 .
1520 (eliminate
1521 NativePhysicalEncodedCommandsResult
1522 (lambda unrestricted current : (family NativePhysicalEncodedCommandsResult) .
1523 (family NativePhysicalImageResult))
1524 (nativePhysicalImageEncodeCommandsForFormat format commands)
1525 (branch
1526 NativePhysicalCommandsEncoded
1527 encoded
1528 .
1529 (eliminate
1530 NativePhysicalEncodedCommands
1531 (lambda unrestricted current : (family NativePhysicalEncodedCommands) .
1532 (family NativePhysicalImageResult))
1533 encoded
1534 (branch
1535 NativePhysicalEncodedCommandsValue
1536 body
1537 commandCount
1538 payloadBytes
1539 auxiliaryBytes
1540 errorBytes
1541 .
1542 (nat-eliminate
1543 (lambda unrestricted current : Nat . (family NativePhysicalImageResult))
1544 (nativePhysicalImageFail
1545 validation
1546 commandCount
1547 (bytes-length body)
1548 (constructor
1549 NativePhysicalImageErrorCode
1550 NativePhysicalImageCommandCountMismatch))
1551 (lambda unrestricted countPredecessor : Nat .
1552 (lambda unrestricted ignoredCount : (family NativePhysicalImageResult) .
1553 (eliminate
1554 NativeTelemetryCounterResult
1555 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1556 (family NativePhysicalImageResult))
1557 (nativeTelemetryCounterFromNatural commandCount)
1558 (branch
1559 NativeTelemetryCounterSucceeded
1560 commandCountWord
1561 .
1562 (eliminate
1563 NativeTelemetryCounterResult
1564 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
1565 (family NativePhysicalImageResult))
1566 (nativeTelemetryCounterFromNatural (bytes-length body))
1567 (branch
1568 NativeTelemetryCounterSucceeded
1569 bodyExtent
1570 .
1571 (app
1572 (lambda unrestricted bodyDigest : Bytes .
1573 (app
1574 (lambda unrestricted output : Bytes .
1575 (app
1576 (lambda unrestricted telemetry : (family NativePhysicalImageTelemetry) .
1577 (constructor
1578 NativePhysicalImageResult
1579 NativePhysicalImageGenerated
1580 (constructor
1581 NativePhysicalImage
1582 NativePhysicalImageValue
1583 output
1584 bodyDigest
1585 identity
1586 commandCount
1587 stateExtent
1588 resultSlots
1589 telemetry)
1590 telemetry))
1591 (nativePhysicalImageTelemetryFor
1592 (nativePhysicalCommandsCounts commands)
1593 payloadBytes
1594 auxiliaryBytes
1595 errorBytes
1596 (bytes-length body)
1597 (bytes-length output)
1598 fallbacks
1599 identity
1600 bodyDigest)))
1601 (bytes-append
1602 (nativePhysicalImageMagicFor format)
1603 (bytes-append
1604 (nativePhysicalImageWord64Bytes (nativePhysicalImageVersionFor format))
1605 (bytes-append
1606 (nativePhysicalImageWord64Bytes commandCountWord)
1607 (bytes-append
1608 (nativePhysicalImageWord64Bytes stateExtent)
1609 (bytes-append
1610 (nativePhysicalImageWord64Bytes resultSlots)
1611 (bytes-append
1612 (nativePhysicalImageWord64Bytes bodyExtent)
1613 (bytes-append identity (bytes-append bodyDigest body))))))))))
1614 (digestOfBody body)))
1615 (branch
1616 NativeTelemetryCounterFailed
1617 counterError
1618 naturalValue
1619 .
1620 (nativePhysicalImageFail
1621 validation
1622 commandCount
1623 (bytes-length body)
1624 (constructor
1625 NativePhysicalImageErrorCode
1626 NativePhysicalImageExtentOverflow)))))
1627 (branch
1628 NativeTelemetryCounterFailed
1629 counterError
1630 naturalValue
1631 .
1632 (nativePhysicalImageFail
1633 validation
1634 commandCount
1635 (bytes-length body)
1636 (constructor
1637 NativePhysicalImageErrorCode
1638 NativePhysicalImageExtentOverflow))))))
1639 (naturalEqual commandCount expected)))))
1640 (branch
1641 NativePhysicalCommandsEncodingFailed
1642 error
1643 ordinal
1644 .
1645 (nativePhysicalImageFail validation ordinal zero error))))))
1646 (branch
1647 NativePhysicalProgramRejected
1648 programError
1649 validation
1650 .
1651 (nativePhysicalImageFail
1652 validation
1653 zero
1654 zero
1655 (constructor
1656 NativePhysicalImageErrorCode
1657 NativePhysicalImageProgramRejected
1658 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.