---- the verdict ----
0 when the plan's device side is certified (see the top of this module)
1782def deviceArenaHazard =
1783 (lambda unrestricted windows : (family ArenaResidents) .
1784 (lambda unrestricted globals : (family ArenaResidents) .
1785 (lambda unrestricted phases : (family DeviceArenaPhases) .
1786 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1787 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1788 (nat-eliminate
1789 (lambda unrestricted placed : Nat . Nat)
1790 1
1791 (lambda unrestricted p : Nat .
1792 (lambda unrestricted ignored : Nat .
1793 (let unrestricted launches =
1794 (deviceArenaLaunches schedule)
1795 in
1796 (let unrestricted words =
1797 (deviceArenaWordsHazard windows globals phases launches)
1798 in
1799 (let unrestricted lifetimes =
1800 (deviceArenaLifetimeHazard
1801 phases
1802 (naturalAdd 2 (deviceArenaLaunchCount launches))
1803 (deviceArenaSubmissionInstances
1804 (deviceArenaRunsOf schedule)
1805 submissions
1806 0
1807 (constructor DeviceArenaInstances DeviceArenaInstancesEnd)))
1808 in
1809 (naturalSelect (naturalIsZero words) lifetimes words))))))
1810 (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.