---- the verdict ----
0 when the plan's device side is certified (see the top of this module)
1763def deviceArenaHazard =
1764 (lambda unrestricted windows : (family ArenaResidents) .
1765 (lambda unrestricted globals : (family ArenaResidents) .
1766 (lambda unrestricted phases : (family DeviceArenaPhases) .
1767 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1768 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1769 (nat-eliminate
1770 (lambda unrestricted placed : Nat . Nat)
1771 1
1772 (lambda unrestricted p : Nat .
1773 (lambda unrestricted ignored : Nat .
1774 (let unrestricted launches =
1775 (deviceArenaLaunches schedule)
1776 in
1777 (let unrestricted words =
1778 (deviceArenaWordsHazard windows globals phases launches)
1779 in
1780 (let unrestricted lifetimes =
1781 (deviceArenaLifetimeHazard
1782 phases
1783 (naturalAdd 2 (deviceArenaLaunchCount launches))
1784 (deviceArenaSubmissionInstances
1785 (deviceArenaRunsOf schedule)
1786 submissions
1787 0
1788 (constructor DeviceArenaInstances DeviceArenaInstancesEnd)))
1789 in
1790 (naturalSelect (naturalIsZero words) lifetimes words))))))
1791 (deviceArenaPlaced globals phases)))))))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.