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