Source operands are evaluated only for selected opportunities. Missing
required words and scope-changing/aliased inputs refuse build; zero is never
manufactured for an omitted observation. Padding alone is explicitly zero.
768def nativeTelemetryCaptureSiteCommand =
769 (lambda unrestricted applicationBytes : Nat .
770 (lambda unrestricted plan : (family TelemetryPolicyPlan) .
771 (lambda unrestricted role : Nat .
772 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
773 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
774 (lambda unrestricted resultSlot : Nat .
775 (lambda unrestricted workSlot : Nat .
776 (lambda unrestricted identity : Bytes .
777 (lambda unrestricted tail : (family NativePhysicalCommands) .
778 (eliminate
779 TelemetryPolicyPlan
780 (lambda unrestricted current : (family TelemetryPolicyPlan) .
781 (family NativePhysicalCommands))
782 plan
783 (branch
784 TelemetryPolicyReady
785 policy
786 ordinarySite
787 reservedSite
788 drain
789 .
790 (eliminate
791 TelemetryDrainPlan
792 (lambda unrestricted current : (family TelemetryDrainPlan) .
793 (family NativePhysicalCommands))
794 drain
795 (branch
796 TelemetryDrainReady
797 ordinaryCapacity
798 reservedCapacity
799 ordinary
800 reserved
801 descriptors
802 bound
803 .
804 (aosChoose
805 (family NativePhysicalCommands)
806 (naturalAnd
807 (naturalLessOrEqual role 1)
808 (naturalAnd
809 (naturalIsZero (naturalEqual resultSlot workSlot))
810 (naturalAnd
811 (telemetryPolicyArenaCertificate
812 applicationBytes
813 ordinaryCapacity
814 reservedCapacity
815 ordinary
816 reserved
817 bound)
818 (naturalAnd
819 (naturalOr
820 (naturalIsZero
821 (captureSiteSelected
822 policy
823 (aosChoose
824 (family CaptureSite)
825 role
826 reservedSite
827 ordinarySite)))
828 (naturalAnd
829 (nativeTelemetrySourcesAdmission
830 (aosChoose
831 (family TelemetryRecordPlan)
832 role
833 reserved
834 ordinary)
835 values)
836 (nativeTelemetrySourceScopesAdmission
837 applicationBytes
838 ordinaryCapacity
839 reservedCapacity
840 (telemetryPolicyDecisionAt
841 applicationBytes
842 ordinaryCapacity
843 reservedCapacity
844 ordinary
845 reserved
846 bound)
847 resultSlot
848 workSlot
849 (aosChoose
850 (family TelemetryRecordPlan)
851 role
852 reserved
853 ordinary)
854 values)))
855 (naturalOr
856 (naturalIsZero
857 (naturalAnd
858 (captureSiteSelected
859 policy
860 (aosChoose
861 (family CaptureSite)
862 role
863 reservedSite
864 ordinarySite))
865 (naturalIsZero
866 (naturalEqual
867 (captureSiteStride
868 (aosChoose
869 (family CaptureSite)
870 role
871 reservedSite
872 ordinarySite))
873 1))))
874 (nativeTelemetrySourceScopeAdmission
875 applicationBytes
876 ordinaryCapacity
877 reservedCapacity
878 (telemetryPolicyDecisionAt
879 applicationBytes
880 ordinaryCapacity
881 reservedCapacity
882 ordinary
883 reserved
884 bound)
885 resultSlot
886 workSlot
887 coordinate))))))
888 (nativeTelemetrySiteCommands
889 applicationBytes
890 policy
891 (aosChoose (family CaptureSite) role reservedSite ordinarySite)
892 ordinaryCapacity
893 reservedCapacity
894 ordinary
895 reserved
896 bound
897 (aosChoose (family TelemetryRecordPlan) role reserved ordinary)
898 values
899 coordinate
900 resultSlot
901 workSlot
902 identity
903 tail)
904 (nativeLaunchRecipeCommand
905 (constructor
906 NativePhysicalOperation
907 NativePhysicalMachineRoutine
908 b""
909 (nativeLaunchRecipeArguments
910 (nativeLaunchRecipeImmediate 0)
911 (nativeLaunchRecipeImmediate 0)
912 (nativeLaunchRecipeImmediate 0)
913 (nativeLaunchRecipeImmediate 0))
914 (constructor
915 NativePhysicalResultBinding
916 NativePhysicalDiscardResult))
917 identity
918 tail)))
919 (branch
920 TelemetryDrainRefused
921 reason
922 .
923 (nativeLaunchRecipeCommand
924 (constructor
925 NativePhysicalOperation
926 NativePhysicalMachineRoutine
927 b""
928 (nativeLaunchRecipeArguments
929 (nativeLaunchRecipeImmediate 0)
930 (nativeLaunchRecipeImmediate 0)
931 (nativeLaunchRecipeImmediate 0)
932 (nativeLaunchRecipeImmediate 0))
933 (constructor
934 NativePhysicalResultBinding
935 NativePhysicalDiscardResult))
936 identity
937 tail))))
938 (branch
939 TelemetryPolicyRefused
940 reason
941 .
942 (nativeLaunchRecipeCommand
943 (constructor
944 NativePhysicalOperation
945 NativePhysicalMachineRoutine
946 b""
947 (nativeLaunchRecipeArguments
948 (nativeLaunchRecipeImmediate 0)
949 (nativeLaunchRecipeImmediate 0)
950 (nativeLaunchRecipeImmediate 0)
951 (nativeLaunchRecipeImmediate 0))
952 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
953 identity
954 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.