Direct operand scopes for a program before adding private residents/slots.
This does not sandbox arbitrary syscall or machine-routine memory effects,
authenticate result-held pointers, or establish runtime argv availability.
Extent tests subtract from admitted ranges; hostile u64 offsets never add.
1456def nativePhysicalOperandScopeAdmission =
1457 (lambda unrestricted stateBytes : Nat .
1458 (lambda unrestricted slots : Nat .
1459 (lambda unrestricted payloadBytes : Nat .
1460 (lambda unrestricted operand : (family NativePhysicalOperand) .
1461 (eliminate
1462 NativePhysicalOperand
1463 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
1464 operand
1465 (branch NativePhysicalImmediate value . 1)
1466 (branch
1467 NativePhysicalResultValue
1468 slot
1469 .
1470 (eliminate
1471 NativePhysicalSlot
1472 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
1473 slot
1474 (branch
1475 NativePhysicalSlotValue
1476 index
1477 .
1478 (naturalLess (modelWord64Natural index) slots))))
1479 (branch
1480 NativePhysicalResultAddress
1481 slot
1482 offset
1483 .
1484 (eliminate
1485 NativePhysicalSlot
1486 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
1487 slot
1488 (branch
1489 NativePhysicalSlotValue
1490 index
1491 .
1492 (naturalLess (modelWord64Natural index) slots))))
1493 (branch
1494 NativePhysicalStateAddress
1495 offset
1496 .
1497 (naturalLess (modelWord64Natural offset) stateBytes))
1498 (branch
1499 NativePhysicalStateLoad64
1500 offset
1501 .
1502 (naturalAnd
1503 (naturalLessOrEqual nativePhysicalWordBytes stateBytes)
1504 (naturalLessOrEqual
1505 (modelWord64Natural offset)
1506 (naturalSaturatingSubtract stateBytes nativePhysicalWordBytes))))
1507 (branch
1508 NativePhysicalPayloadAddress
1509 offset
1510 .
1511 (naturalLess (modelWord64Natural offset) payloadBytes))
1512 (branch
1513 NativePhysicalPayloadLoad64
1514 offset
1515 .
1516 (naturalAnd
1517 (naturalLessOrEqual nativePhysicalWordBytes payloadBytes)
1518 (naturalLessOrEqual
1519 (modelWord64Natural offset)
1520 (naturalSaturatingSubtract payloadBytes nativePhysicalWordBytes))))
1521 (branch NativePhysicalProcessArgument index . 1)
1522 (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.