1600def nativePhysicalOperationScopeAdmission =
1601 (lambda unrestricted stateBytes : Nat .
1602 (lambda unrestricted slots : Nat .
1603 (lambda unrestricted operation : (family NativePhysicalOperation) .
1604 (eliminate
1605 NativePhysicalOperation
1606 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
1607 operation
1608 (branch
1609 NativePhysicalSystemCall
1610 number
1611 arguments
1612 payload
1613 result
1614 .
1615 (naturalAnd
1616 (nativePhysicalOperandScopeAdmission stateBytes slots 0 number)
1617 (naturalAnd
1618 (nativePhysicalArgumentsScopeAdmission
1619 stateBytes
1620 slots
1621 (bytes-length payload)
1622 arguments)
1623 (naturalAnd (nativePhysicalResultScopeAdmission slots result) 1))))
1624 (branch
1625 NativePhysicalCopyPayloadToState
1626 destination
1627 extent
1628 payload
1629 .
1630 (naturalAnd
1631 (naturalAnd
1632 (naturalLessOrEqual (modelWord64Natural extent) stateBytes)
1633 (naturalLessOrEqual
1634 (modelWord64Natural destination)
1635 (naturalSaturatingSubtract stateBytes (modelWord64Natural extent))))
1636 (naturalAnd (naturalEqual (modelWord64Natural extent) (bytes-length payload)) 1)))
1637 (branch
1638 NativePhysicalMachineRoutine
1639 code
1640 arguments
1641 result
1642 .
1643 (naturalAnd
1644 (nativePhysicalArgumentsScopeAdmission stateBytes slots (bytes-length code) arguments)
1645 (naturalAnd (nativePhysicalResultScopeAdmission slots result) 1)))
1646 (branch
1647 NativePhysicalFencePoll
1648 address
1649 expected
1650 polls
1651 .
1652 (naturalAnd
1653 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes address)
1654 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected) 1)))
1655 (branch NativePhysicalTelemetryAppend path record . 1)
1656 (branch
1657 NativePhysicalAssertEqual
1658 left
1659 right
1660 error
1661 .
1662 (naturalAnd
1663 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1664 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1)))
1665 (branch
1666 NativePhysicalAssertOneOf
1667 observed
1668 first
1669 second
1670 error
1671 .
1672 (naturalAnd
1673 (nativePhysicalOperandScopeAdmission stateBytes slots 0 observed)
1674 (naturalAnd
1675 (nativePhysicalOperandScopeAdmission stateBytes slots 0 first)
1676 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 second) 1))))
1677 (branch NativePhysicalHaltSuccess . 1)
1678 (branch NativePhysicalRepeatBegin count . 1)
1679 (branch
1680 NativePhysicalSkipUnlessEqual
1681 left
1682 right
1683 count
1684 .
1685 (naturalAnd
1686 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1687 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1)))
1688 (branch NativePhysicalRepeatEnd . 1)
1689 (branch
1690 NativePhysicalRepeatEndWhen
1691 observed
1692 expected
1693 .
1694 (naturalAnd
1695 (nativePhysicalOperandScopeAdmission stateBytes slots 0 observed)
1696 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected) 1)))
1697 (branch
1698 NativePhysicalStoreWord64
1699 destination
1700 value
1701 .
1702 (naturalAnd
1703 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1704 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 value) 1)))
1705 (branch
1706 NativePhysicalFenceWait
1707 address
1708 expected
1709 polls
1710 interval
1711 .
1712 (naturalAnd
1713 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes address)
1714 (naturalAnd
1715 (nativePhysicalOperandScopeAdmission stateBytes slots 0 expected)
1716 (naturalAnd
1717 1
1718 (naturalAnd 1 1)))))
1719 (branch
1720 NativePhysicalRepeatBeginCounted
1721 count
1722 .
1723 (nativePhysicalOperandScopeAdmission stateBytes slots 0 count))
1724 (branch
1725 NativePhysicalAddWord64
1726 destination
1727 left
1728 right
1729 .
1730 (naturalAnd
1731 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1732 (naturalAnd
1733 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1734 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1))))
1735 (branch
1736 NativePhysicalFloat64
1737 operation
1738 destination
1739 left
1740 right
1741 .
1742 (naturalAnd
1743 (nativePhysicalAddressSpanAdmission stateBytes slots nativePhysicalWordBytes destination)
1744 (naturalAnd
1745 (nativePhysicalOperandScopeAdmission stateBytes slots 0 left)
1746 (naturalAnd (nativePhysicalOperandScopeAdmission stateBytes slots 0 right) 1))))))))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.