624def telemetryDispatchPlan =
625 (lambda unrestricted ordinaryCapacity : Nat .
626 (lambda unrestricted reservedCapacity : Nat .
627 (lambda unrestricted ordinary : (family TelemetryRouteDeclarations) .
628 (lambda unrestricted reserved : (family TelemetryRouteDeclarations) .
629 (lambda unrestricted descriptors : (family StdList Bytes) .
630 (let unrestricted ordinaryRoutes =
631 (telemetryCompileRecordRoutes ordinary)
632 in
633 (let unrestricted reservedRoutes =
634 (telemetryCompileRecordRoutes reserved)
635 in
636 (let unrestricted ordinaryMaximum =
637 (telemetryRouteMaximumRecord ordinaryRoutes)
638 in
639 (let unrestricted reservedMaximum =
640 (telemetryRouteMaximumRecord reservedRoutes)
641 in
642 (let unrestricted descriptorBytes =
643 (publicationTypedRecordBytes descriptors)
644 in
645 (let unrestricted bound =
646 (telemetryDrainBound
647 ordinaryCapacity
648 reservedCapacity
649 ordinaryMaximum
650 reservedMaximum
651 descriptorBytes)
652 in
653 (aosChoose
654 (family TelemetryDispatchPlan)
655 (naturalAnd
656 (naturalLessOrEqual 2 reservedCapacity)
657 (naturalAnd
658 (naturalLessOrEqual
659 (naturalAdd
660 (naturalAdd ordinaryCapacity reservedCapacity)
661 (aosListLength descriptors))
662 1024)
663 (naturalAnd
664 (naturalLessOrEqual
665 (naturalAdd
666 (telemetryRouteDeclarationsCount ordinary)
667 (telemetryRouteDeclarationsCount reserved))
668 1024)
669 (naturalAnd
670 (naturalOr
671 (naturalIsZero ordinaryCapacity)
672 (naturalNonzero (telemetryDrainRecordBytes ordinaryMaximum)))
673 (naturalAnd
674 -- Reserved capacity protects recorder bookkeeping even
675 -- when this program declares no reserved event routes.
676 -- An empty route inventory cannot enqueue a reserved
677 -- record; every declared route still needs a valid plan.
678 (naturalOr
679 (naturalIsZero (telemetryRouteDeclarationsCount reserved))
680 (naturalNonzero (telemetryDrainRecordBytes reservedMaximum)))
681 (naturalAnd
682 (telemetryDrainDescriptorsAdmission descriptors)
683 (naturalAnd
684 (telemetryRouteDeclarationsAdmission
685 ordinary
686 reserved
687 descriptors)
688 (naturalAnd
689 (telemetryRouteDeclarationsAdmission
690 reserved
691 ordinary
692 descriptors)
693 (naturalLessOrEqual
694 (publicationRecordBytes bound)
695 publicationMaximumFrameBytes)))))))))
696 (constructor
697 TelemetryDispatchPlan
698 TelemetryDispatchReady
699 ordinaryCapacity
700 reservedCapacity
701 ordinaryRoutes
702 reservedRoutes
703 ordinaryMaximum
704 reservedMaximum
705 descriptorBytes
706 bound)
707 (constructor
708 TelemetryDispatchPlan
709 TelemetryDispatchRefused
710 b"native-typed-route-declaration-refused")))))))))))))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.