1776def greedyArgmaxSM86BuildEncoded =
1777 (lambda unrestricted program : (family SM86Program) .
1778 (lambda unrestricted manifest : (family GreedyArgmaxSM86Manifest) .
1779 (eliminate
1780 SM86ProgramEncodingResult
1781 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
1782 (family GreedyArgmaxSM86Artifact))
1783 (sm86EncodeProgram program)
1784 (branch
1785 SM86ProgramEncodingSucceeded
1786 image
1787 telemetry
1788 .
1789 (eliminate
1790 SM86ProgramEncodingTelemetry
1791 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
1792 (family GreedyArgmaxSM86Artifact))
1793 telemetry
1794 (branch
1795 SM86ProgramEncodingTelemetryValue
1796 instructions
1797 encodedBytes
1798 fields
1799 bits
1800 highest
1801 .
1802 (eliminate
1803 GreedyArgmaxSM86Manifest
1804 (lambda unrestricted current : (family GreedyArgmaxSM86Manifest) .
1805 (family GreedyArgmaxSM86Artifact))
1806 manifest
1807 (branch
1808 GreedyArgmaxSM86ManifestValue
1809 vocabulary
1810 fullSlots
1811 tailLanes
1812 expectedInstructions
1813 expectedBytes
1814 registers
1815 sharedBytes
1816 gridX
1817 threads
1818 activeLoads
1819 activeFinite
1820 inactiveFinite
1821 tailMasks
1822 tieStages
1823 tokenWrites
1824 validityWrites
1825 hostReads
1826 fallbacks
1827 abi
1828 .
1829 (nat-eliminate
1830 (lambda unrestricted instructionsExact : Nat .
1831 (family GreedyArgmaxSM86Artifact))
1832 (greedyArgmaxSM86Failed
1833 manifest
1834 (constructor
1835 GreedyArgmaxSM86FailureCode
1836 GreedyArgmaxSM86EncodedInstructionCountMismatch)
1837 instructions
1838 instructions
1839 encodedBytes)
1840 (lambda unrestricted instructionPredecessor : Nat .
1841 (lambda unrestricted instructionInduction : (family GreedyArgmaxSM86Artifact) .
1842 (nat-eliminate
1843 (lambda unrestricted bytesExact : Nat . (family GreedyArgmaxSM86Artifact))
1844 (greedyArgmaxSM86Failed
1845 manifest
1846 (constructor
1847 GreedyArgmaxSM86FailureCode
1848 GreedyArgmaxSM86EncodedByteCountMismatch)
1849 encodedBytes
1850 instructions
1851 encodedBytes)
1852 (lambda unrestricted bytePredecessor : Nat .
1853 (lambda unrestricted byteInduction : (family GreedyArgmaxSM86Artifact) .
1854 (greedyArgmaxSM86BuildIdentity program image manifest telemetry)))
1855 (naturalEqual encodedBytes expectedBytes))))
1856 (naturalEqual instructions expectedInstructions)))))))
1857 (branch
1858 SM86ProgramEncodingFailed
1859 instructionIndex
1860 failure
1861 telemetry
1862 .
1863 (greedyArgmaxSM86Failed
1864 manifest
1865 (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86ImageEncodingFailed)
1866 instructionIndex
1867 (sm86ProgramCount program)
1868 zero)))))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.