1696def deviceArenaLifetimeHazard =
1697 (lambda unrestricted phases : (family DeviceArenaPhases) .
1698 (lambda unrestricted base : Nat .
1699 (lambda unrestricted instances : (family DeviceArenaInstances) .
1700 (let unrestricted carried =
1701 (deviceArenaCarriedAnywhere phases)
1702 in
1703 (app
1704 (eliminate
1705 DeviceArenaInstances
1706 (lambda unrestricted current : (family DeviceArenaInstances) .
1707 (pi unrestricted tracked : (family DeviceArenaTracked) .
1708 (pi unrestricted previous : Bytes . (pi unrestricted index : Nat . Nat))))
1709 instances
1710 (branch
1711 DeviceArenaInstancesEnd
1712 .
1713 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1714 (lambda unrestricted previous : Bytes . (lambda unrestricted index : Nat . 0))))
1715 (branch
1716 DeviceArenaInstancesNext
1717 identity
1718 tail
1719 induction
1720 .
1721 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1722 (lambda unrestricted previous : Bytes .
1723 (lambda unrestricted index : Nat .
1724 (let unrestricted starts =
1725 (naturalIsZero (bytes-equal identity previous))
1726 in
1727 (let unrestricted phase =
1728 (deviceArenaPhaseOf phases identity)
1729 in
1730 (let unrestricted broken =
1731 (naturalAnd
1732 starts
1733 (naturalIsZero
1734 (deviceArenaAllIntact tracked (deviceArenaPhaseCarriedOf phase))))
1735 in
1736 (let unrestricted next =
1737 (nat-eliminate
1738 (lambda unrestricted fresh : Nat . (family DeviceArenaTracked))
1739 tracked
1740 (lambda unrestricted q : Nat .
1741 (lambda unrestricted unused : (family DeviceArenaTracked) .
1742 (deviceArenaDeclare
1743 carried
1744 tracked
1745 (deviceArenaPhasePlanes phase))))
1746 starts)
1747 in
1748 (let unrestricted later =
1749 (induction next identity (naturalAdd index starts))
1750 in
1751 (nat-eliminate
1752 (lambda unrestricted found : Nat . Nat)
1753 later
1754 (lambda unrestricted q : Nat .
1755 (lambda unrestricted unused : Nat . (naturalAdd base index)))
1756 broken)))))))))))
1757 deviceArenaTrackedEnd
1758 b"\x00"
1759 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.