A pointer operand's start may be valid while an eight-byte operation at
it crosses into the next resident. Check known direct ranges at the use's
width; indirect/result-held pointers retain their explicit primitive trust.
1577def nativePhysicalAddressSpanAdmission =
1578 (lambda unrestricted stateBytes : Nat .
1579 (lambda unrestricted slots : Nat .
1580 (lambda unrestricted width : Nat .
1581 (lambda unrestricted operand : (family NativePhysicalOperand) .
1582 (eliminate NativePhysicalOperand
1583 (lambda unrestricted current : (family NativePhysicalOperand) . Nat) operand
1584 (branch NativePhysicalImmediate value . 1)
1585 (branch NativePhysicalResultValue slot .
1586 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1587 (branch NativePhysicalResultAddress slot offset .
1588 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1589 (branch NativePhysicalStateAddress offset .
1590 (naturalAnd (naturalLessOrEqual width stateBytes)
1591 (naturalLessOrEqual (modelWord64Natural offset)
1592 (naturalSaturatingSubtract stateBytes width))))
1593 (branch NativePhysicalStateLoad64 offset .
1594 (nativePhysicalOperandScopeAdmission stateBytes slots 0 operand))
1595 (branch NativePhysicalPayloadAddress offset . 0)
1596 (branch NativePhysicalPayloadLoad64 offset . 0)
1597 (branch NativePhysicalProcessArgument index . 1)
1598 (branch NativePhysicalLoopAffine base stride . 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.