1711def greedyArgmaxSM86BuildIdentity =
1712 (lambda unrestricted program : (family SM86Program) .
1713 (lambda unrestricted image : Bytes .
1714 (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1715 (lambda unrestricted encodingTelemetry : (family SM86ProgramEncodingTelemetry) .
1716 (eliminate
1717 SM86ProgramEncodingTelemetry
1718 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1719 (family GreedyArgmaxSM86Artifact))
1720 encodingTelemetry
1721 (branch
1722 SM86ProgramEncodingTelemetryValue
1723 instructions
1724 encodedBytes
1725 fields
1726 bits
1727 highest
1728 .
1729 (eliminate
1730 SHA256HexResult
1731 (lambda unrestricted current : (family SHA256HexResult) .
1732 (family GreedyArgmaxSM86Artifact))
1733 (sha256Hex image)
1734 (branch
1735 SHA256HexSucceeded
1736 identity
1737 digestTelemetry
1738 .
1739 (nat-eliminate
1740 (lambda unrestricted exactLength : Nat . (family GreedyArgmaxSM86Artifact))
1741 (greedyArgmaxSM86Failed
1742 manifest
1743 (constructor
1744 GreedyArgmaxSM86FailureCode
1745 GreedyArgmaxSM86ImageIdentityLengthInvalid)
1746 (bytes-length identity)
1747 instructions
1748 encodedBytes)
1749 (lambda unrestricted predecessor : Nat .
1750 (lambda unrestricted induction : (family GreedyArgmaxSM86Artifact) .
1751 (constructor
1752 GreedyArgmaxSM86Artifact
1753 GreedyArgmaxSM86ArtifactReady
1754 program
1755 image
1756 identity
1757 manifest
1758 encodingTelemetry
1759 digestTelemetry
1760 (greedyArgmaxSM86TelemetryFor
1761 manifest
1762 instructions
1763 encodedBytes
1764 fields
1765 bits
1766 highest
1767 (bytes-length image)
1768 (bytes-length identity)))))
1769 (naturalEqual (bytes-length identity) greedyArgmaxSM86N64)))
1770 (branch
1771 SHA256HexFailed
1772 failure
1773 hexFailureOrdinal
1774 digestTelemetry
1775 .
1776 (greedyArgmaxSM86Failed
1777 manifest
1778 (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageIdentityFailed)
1779 zero
1780 instructions
1781 encodedBytes)))))))))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.