933def nativeTelemetryDispatchCaptureCommand =
934 (lambda unrestricted applicationBytes : Nat .
935 (lambda unrestricted plan : (family TelemetryDispatchPlan) .
936 (lambda unrestricted selected : Nat .
937 (lambda unrestricted role : Nat .
938 (lambda unrestricted tag : Nat .
939 (lambda unrestricted resultSlot : Nat .
940 (lambda unrestricted identity : Bytes .
941 (lambda unrestricted tail : (family NativePhysicalCommands) .
942 (eliminate
943 TelemetryDispatchPlan
944 (lambda unrestricted current : (family TelemetryDispatchPlan) .
945 (family NativePhysicalCommands))
946 plan
947 (branch
948 TelemetryDispatchReady
949 ordinaryCapacity
950 reservedCapacity
951 ordinaryRoutes
952 reservedRoutes
953 ordinary
954 reserved
955 descriptors
956 bound
957 .
958 (aosChoose
959 (family NativePhysicalCommands)
960 (naturalAnd
961 (naturalLessOrEqual role 1)
962 (naturalAnd
963 (naturalLessOrEqual selected 1)
964 (naturalAnd
965 (telemetryDispatchArenaCertificate
966 applicationBytes
967 ordinaryCapacity
968 reservedCapacity
969 ordinary
970 reserved
971 bound)
972 (telemetryRecordRouteContains
973 tag
974 (aosChoose
975 (family TelemetryRecordRoutes)
976 role
977 reservedRoutes
978 ordinaryRoutes)))))
979 (nativeTelemetryCaptureCommand
980 applicationBytes
981 ordinaryCapacity
982 reservedCapacity
983 selected
984 role
985 resultSlot
986 identity
987 (nativeLaunchRecipeCommand
988 (constructor
989 NativePhysicalOperation
990 NativePhysicalMachineRoutine
991 (drainCommitTagRoutine ordinaryCapacity reservedCapacity role tag)
992 (constructor
993 NativePhysicalArguments
994 NativePhysicalArgumentsValue
995 (drainState (captureControlAt applicationBytes))
996 (drainState
997 (telemetryDispatchTagsAt
998 applicationBytes
999 ordinaryCapacity
1000 reservedCapacity
1001 ordinary
1002 reserved
1003 bound))
1004 (nativeLaunchRecipeSlotValue resultSlot)
1005 (nativeLaunchRecipeImmediate
1006 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))
1007 (nativeLaunchRecipeImmediate 0)
1008 (nativeLaunchRecipeImmediate 0))
1009 (nativeLaunchRecipeStore resultSlot))
1010 identity
1011 tail))
1012 (nativeLaunchRecipeCommand
1013 (constructor
1014 NativePhysicalOperation
1015 NativePhysicalMachineRoutine
1016 b""
1017 (constructor
1018 NativePhysicalArguments
1019 NativePhysicalArgumentsValue
1020 (nativeLaunchRecipeImmediate 0)
1021 (nativeLaunchRecipeImmediate 0)
1022 (nativeLaunchRecipeImmediate 0)
1023 (nativeLaunchRecipeImmediate 0)
1024 (nativeLaunchRecipeImmediate 0)
1025 (nativeLaunchRecipeImmediate 0))
1026 (nativeLaunchRecipeStore resultSlot))
1027 identity
1028 tail)))
1029 (branch
1030 TelemetryDispatchRefused
1031 reason
1032 .
1033 (nativeLaunchRecipeCommand
1034 (constructor
1035 NativePhysicalOperation
1036 NativePhysicalMachineRoutine
1037 b""
1038 (constructor
1039 NativePhysicalArguments
1040 NativePhysicalArgumentsValue
1041 (nativeLaunchRecipeImmediate 0)
1042 (nativeLaunchRecipeImmediate 0)
1043 (nativeLaunchRecipeImmediate 0)
1044 (nativeLaunchRecipeImmediate 0)
1045 (nativeLaunchRecipeImmediate 0)
1046 (nativeLaunchRecipeImmediate 0))
1047 (nativeLaunchRecipeStore resultSlot))
1048 identity
1049 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.