1715def deviceArenaLifetimeHazard =
1716 (lambda unrestricted phases : (family DeviceArenaPhases) .
1717 (lambda unrestricted base : Nat .
1718 (lambda unrestricted instances : (family DeviceArenaInstances) .
1719 (let unrestricted carried =
1720 (deviceArenaCarriedAnywhere phases)
1721 in
1722 (app
1723 (eliminate
1724 DeviceArenaInstances
1725 (lambda unrestricted current : (family DeviceArenaInstances) .
1726 (pi unrestricted tracked : (family DeviceArenaTracked) .
1727 (pi unrestricted previous : Bytes . (pi unrestricted index : Nat . Nat))))
1728 instances
1729 (branch
1730 DeviceArenaInstancesEnd
1731 .
1732 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1733 (lambda unrestricted previous : Bytes . (lambda unrestricted index : Nat . 0))))
1734 (branch
1735 DeviceArenaInstancesNext
1736 identity
1737 tail
1738 induction
1739 .
1740 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1741 (lambda unrestricted previous : Bytes .
1742 (lambda unrestricted index : Nat .
1743 (let unrestricted starts =
1744 (naturalIsZero (bytes-equal identity previous))
1745 in
1746 (let unrestricted phase =
1747 (deviceArenaPhaseOf phases identity)
1748 in
1749 (let unrestricted broken =
1750 (naturalAnd
1751 starts
1752 (naturalIsZero
1753 (deviceArenaAllIntact tracked (deviceArenaPhaseCarriedOf phase))))
1754 in
1755 (let unrestricted next =
1756 (nat-eliminate
1757 (lambda unrestricted fresh : Nat . (family DeviceArenaTracked))
1758 tracked
1759 (lambda unrestricted q : Nat .
1760 (lambda unrestricted unused : (family DeviceArenaTracked) .
1761 (deviceArenaDeclare
1762 carried
1763 tracked
1764 (deviceArenaPhasePlanes phase))))
1765 starts)
1766 in
1767 (let unrestricted later =
1768 (induction next identity (naturalAdd index starts))
1769 in
1770 (nat-eliminate
1771 (lambda unrestricted found : Nat . Nat)
1772 later
1773 (lambda unrestricted q : Nat .
1774 (lambda unrestricted unused : Nat . (naturalAdd base index)))
1775 broken)))))))))))
1776 deviceArenaTrackedEnd
1777 b"\x00"
1778 0)))))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.