1397def nativeTelemetryRoutedCaptureSiteCommand =
1398 (lambda unrestricted applicationBytes : Nat .
1399 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
1400 (lambda unrestricted wanted : Nat .
1401 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
1402 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
1403 (lambda unrestricted resultSlot : Nat .
1404 (lambda unrestricted workSlot : Nat .
1405 (lambda unrestricted identity : Bytes .
1406 (lambda unrestricted tail : (family NativePhysicalCommands) .
1407 (eliminate
1408 TelemetryRoutedPolicyPlan
1409 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) .
1410 (family NativePhysicalCommands))
1411 plan
1412 (branch
1413 TelemetryRoutedPolicyReady
1414 policy
1415 sites
1416 drain
1417 .
1418 (eliminate
1419 TelemetryDispatchPlan
1420 (lambda unrestricted current : (family TelemetryDispatchPlan) .
1421 (family NativePhysicalCommands))
1422 drain
1423 (branch
1424 TelemetryDispatchReady
1425 ordinaryCapacity
1426 reservedCapacity
1427 ordinaryRoutes
1428 reservedRoutes
1429 ordinary
1430 reserved
1431 descriptors
1432 bound
1433 .
1434 (eliminate
1435 TelemetryPolicySites
1436 (lambda unrestricted current : (family TelemetryPolicySites) .
1437 (family NativePhysicalCommands))
1438 (telemetryPolicySiteLookup wanted sites)
1439 (branch
1440 TelemetryPolicySitesEnd
1441 .
1442 (nativeLaunchRecipeCommand
1443 (constructor
1444 NativePhysicalOperation
1445 NativePhysicalMachineRoutine
1446 b""
1447 (constructor
1448 NativePhysicalArguments
1449 NativePhysicalArgumentsValue
1450 (nativeLaunchRecipeImmediate 0)
1451 (nativeLaunchRecipeImmediate 0)
1452 (nativeLaunchRecipeImmediate 0)
1453 (nativeLaunchRecipeImmediate 0)
1454 (nativeLaunchRecipeImmediate 0)
1455 (nativeLaunchRecipeImmediate 0))
1456 (nativeLaunchRecipeStore resultSlot))
1457 identity
1458 tail))
1459 (branch
1460 TelemetryPolicySitesNext
1461 tag
1462 site
1463 declaration
1464 following
1465 induction
1466 .
1467 (let unrestricted recipe =
1468 (telemetryRecordRouteLookup
1469 tag
1470 (aosChoose
1471 (family TelemetryRecordRoutes)
1472 (captureSiteReserved site)
1473 reservedRoutes
1474 ordinaryRoutes))
1475 in
1476 (aosChoose
1477 (family NativePhysicalCommands)
1478 (naturalAnd
1479 (telemetryRoutedPolicyArenaCertificate
1480 applicationBytes
1481 ordinaryCapacity
1482 reservedCapacity
1483 ordinary
1484 reserved
1485 bound)
1486 (naturalAnd
1487 (naturalIsZero (naturalEqual resultSlot workSlot))
1488 (naturalAnd
1489 (naturalOr
1490 (naturalIsZero (captureSiteSelected policy site))
1491 (naturalAnd
1492 (nativeTelemetrySourcesAdmission recipe values)
1493 (nativeTelemetrySourceScopesWith
1494 recipe
1495 values
1496 (nativeTelemetryRoutedSourceScopeAdmission
1497 applicationBytes
1498 ordinaryCapacity
1499 reservedCapacity
1500 ordinary
1501 reserved
1502 bound
1503 resultSlot
1504 workSlot))))
1505 (naturalOr
1506 (naturalIsZero
1507 (naturalAnd
1508 (captureSiteSelected policy site)
1509 (naturalIsZero (naturalEqual (captureSiteStride site) 1))))
1510 (nativeTelemetryRoutedSourceScopeAdmission
1511 applicationBytes
1512 ordinaryCapacity
1513 reservedCapacity
1514 ordinary
1515 reserved
1516 bound
1517 resultSlot
1518 workSlot
1519 coordinate)))))
1520 (nativeTelemetrySiteWith
1521 applicationBytes
1522 policy
1523 site
1524 ordinaryCapacity
1525 reservedCapacity
1526 bound
1527 (telemetryRoutedPolicyDecisionAt
1528 applicationBytes
1529 ordinaryCapacity
1530 reservedCapacity
1531 ordinary
1532 reserved
1533 bound)
1534 recipe
1535 values
1536 coordinate
1537 resultSlot
1538 workSlot
1539 identity
1540 (lambda unrestricted commands : (family NativePhysicalCommands) .
1541 (nativeTelemetryCaptureSelectedCommand
1542 applicationBytes
1543 ordinaryCapacity
1544 reservedCapacity
1545 (nativeTelemetryPolicyLoad
1546 (telemetryRoutedPolicyDecisionAt
1547 applicationBytes
1548 ordinaryCapacity
1549 reservedCapacity
1550 ordinary
1551 reserved
1552 bound))
1553 (captureSiteReserved site)
1554 resultSlot
1555 identity
1556 (nativeLaunchRecipeCommand
1557 (constructor
1558 NativePhysicalOperation
1559 NativePhysicalMachineRoutine
1560 (drainCommitTagRoutine
1561 ordinaryCapacity
1562 reservedCapacity
1563 (captureSiteReserved site)
1564 tag)
1565 (constructor
1566 NativePhysicalArguments
1567 NativePhysicalArgumentsValue
1568 (nativeTelemetryPolicyState
1569 (captureControlAt applicationBytes))
1570 (nativeTelemetryPolicyState
1571 (telemetryDispatchTagsAt
1572 applicationBytes
1573 ordinaryCapacity
1574 reservedCapacity
1575 ordinary
1576 reserved
1577 bound))
1578 (nativeLaunchRecipeSlotValue resultSlot)
1579 (nativeLaunchRecipeImmediate
1580 (telemetryDispatchTagsBytes
1581 ordinaryCapacity
1582 reservedCapacity))
1583 (nativeLaunchRecipeImmediate 0)
1584 (nativeLaunchRecipeImmediate 0))
1585 (nativeLaunchRecipeStore resultSlot))
1586 identity
1587 commands)))
1588 tail)
1589 (nativeLaunchRecipeCommand
1590 (constructor
1591 NativePhysicalOperation
1592 NativePhysicalMachineRoutine
1593 b""
1594 (constructor
1595 NativePhysicalArguments
1596 NativePhysicalArgumentsValue
1597 (nativeLaunchRecipeImmediate 0)
1598 (nativeLaunchRecipeImmediate 0)
1599 (nativeLaunchRecipeImmediate 0)
1600 (nativeLaunchRecipeImmediate 0)
1601 (nativeLaunchRecipeImmediate 0)
1602 (nativeLaunchRecipeImmediate 0))
1603 (nativeLaunchRecipeStore resultSlot))
1604 identity
1605 tail))))))
1606 (branch
1607 TelemetryDispatchRefused
1608 reason
1609 .
1610 (nativeLaunchRecipeCommand
1611 (constructor
1612 NativePhysicalOperation
1613 NativePhysicalMachineRoutine
1614 b""
1615 (constructor
1616 NativePhysicalArguments
1617 NativePhysicalArgumentsValue
1618 (nativeLaunchRecipeImmediate 0)
1619 (nativeLaunchRecipeImmediate 0)
1620 (nativeLaunchRecipeImmediate 0)
1621 (nativeLaunchRecipeImmediate 0)
1622 (nativeLaunchRecipeImmediate 0)
1623 (nativeLaunchRecipeImmediate 0))
1624 (nativeLaunchRecipeStore resultSlot))
1625 identity
1626 tail))))
1627 (branch
1628 TelemetryRoutedPolicyRefused
1629 reason
1630 .
1631 (nativeLaunchRecipeCommand
1632 (constructor
1633 NativePhysicalOperation
1634 NativePhysicalMachineRoutine
1635 b""
1636 (constructor
1637 NativePhysicalArguments
1638 NativePhysicalArgumentsValue
1639 (nativeLaunchRecipeImmediate 0)
1640 (nativeLaunchRecipeImmediate 0)
1641 (nativeLaunchRecipeImmediate 0)
1642 (nativeLaunchRecipeImmediate 0)
1643 (nativeLaunchRecipeImmediate 0)
1644 (nativeLaunchRecipeImmediate 0))
1645 (nativeLaunchRecipeStore resultSlot))
1646 identity
1647 tail))))))))))))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.