Call at a declared safe boundary. Capture and publication outcomes stay
separate. Pending values must be retried after a nonterminal acknowledgement;
a terminal request while pending refuses to invent producer completion.
1128def nativeTelemetryPolicyBoundaryWith =
1129 (lambda unrestricted applicationBytes : Nat .
1130 (lambda unrestricted ordinaryCapacity : Nat .
1131 (lambda unrestricted reservedCapacity : Nat .
1132 (lambda unrestricted bound : Nat .
1133 (lambda unrestricted threshold : Nat .
1134 (lambda unrestricted decisionAt : Nat .
1135 (lambda unrestricted terminal : Nat .
1136 (lambda unrestricted captureSlot : Nat .
1137 (lambda unrestricted publicationSlot : Nat .
1138 (lambda unrestricted workSlot : Nat .
1139 (lambda unrestricted identity : Bytes .
1140 (lambda unrestricted drain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1141 (lambda unrestricted tail : (family NativePhysicalCommands) .
1142 (nativeLaunchRecipeCommand
1143 (constructor
1144 NativePhysicalOperation
1145 NativePhysicalMachineRoutine
1146 (nativeTelemetryPolicyFlushRoutine threshold bound)
1147 (constructor
1148 NativePhysicalArguments
1149 NativePhysicalArgumentsValue
1150 (nativeTelemetryPolicyState (captureControlAt applicationBytes))
1151 (nativeTelemetryPolicyState
1152 (publicationBase
1153 applicationBytes
1154 ordinaryCapacity
1155 reservedCapacity))
1156 (nativeLaunchRecipeSlotValue captureSlot)
1157 (nativeLaunchRecipeImmediate terminal)
1158 (nativeTelemetryPolicyState decisionAt)
1159 (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound)))
1160 (nativeLaunchRecipeStore workSlot))
1161 identity
1162 (nativeLaunchRecipeCommand
1163 (constructor
1164 NativePhysicalOperation
1165 NativePhysicalMachineRoutine
1166 recordStatusRoutine
1167 (nativeLaunchRecipeArguments
1168 (nativeTelemetryPolicyState decisionAt)
1169 (nativeLaunchRecipeImmediate 0)
1170 (nativeLaunchRecipeImmediate 0)
1171 (nativeLaunchRecipeImmediate 0))
1172 (nativeLaunchRecipeStore publicationSlot))
1173 identity
1174 (nativeLaunchRecipeCommand
1175 (constructor
1176 NativePhysicalOperation
1177 NativePhysicalRepeatBeginCounted
1178 (nativeLaunchRecipeSlotValue workSlot))
1179 identity
1180 (drain
1181 (nativeLaunchRecipeCommand
1182 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
1183 identity
1184 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.