module Runtime.NativeTelemetryDrain import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Data.Bytes import Model.Word64 import Observe.Value import Runtime.NativeLaunchRecipeLoad import Runtime.NativeMemoryRoutine import Runtime.NativePhysicalProgram import Runtime.NativeTelemetry import Runtime.NativeTelemetryCapture import Runtime.NativeTelemetryPublication import Runtime.NativeTelemetryRecord import Runtime.NativeTelemetrySeal import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryDrainRoutine import Runtime.TelemetryIdentity import Runtime.TelemetryPublication import Runtime.TelemetryRecord import Std.Natural import Runtime.NativeWordDigest -- System V realization of shared staging/tag semantics. Registers and -- instruction choices preserve the existing routine identities. def drainX86JumpIf = (lambda unrestricted condition : (family TelemetryDrainCondition) . (digestJumpIf (eliminate TelemetryDrainCondition (lambda unrestricted current : (family TelemetryDrainCondition) . (family X86NativeCondition)) condition (branch TelemetryDrainZero . (constructor X86NativeCondition X86NativeConditionZero)) (branch TelemetryDrainNotZero . (constructor X86NativeCondition X86NativeConditionNotZero)) (branch TelemetryDrainBelow . (constructor X86NativeCondition X86NativeConditionBelow)) (branch TelemetryDrainAbove . (constructor X86NativeCondition X86NativeConditionAbove))))) def drainX86Divide = (lambda unrestricted divisor : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeDivideRegister64Unsigned divisor))) def drainX86Backend = (constructor TelemetryDrainBackend TelemetryDrainBackendValue (family X86NativeAssembly) (family X86NativeRegister64) digestMovImm digestMov digestLoad64 digestStore64 digestStore8 digestCmpImm publicationCompare publicationSubtract digestAdd digestAddImm digestMulImm drainX86Divide drainX86JumpIf publicationJump digestLabel digestReturn digestEnd digestRAX digestRDI digestRSI digestRDX digestRCX digestR8 digestR9 digestR10 digestR11) def nativeTelemetryDrainRoutineFor = (lambda unrestricted kind : (family TelemetryDrainRoutineKind) . (compiler-native-encode (family X86NativeAssembly) (telemetryDrainAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) drainX86Backend kind))) -- A single writer drains the occupied prefixes at a safe boundary. No record -- formatting occurs in acquisition. Source pointers advance only after a -- rendered record has passed append preflight and its bytes have been copied. -- Private saved-register cells are cursor scratch until the shared commit -- owner uses them; no commit or acquisition may run concurrently with a drain. def drainReadyAssembly : (family X86NativeAssembly) = (telemetryDrainAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) drainX86Backend (constructor TelemetryDrainRoutineKind TelemetryDrainReadyRoutine)) def drainReadyRoutine : Bytes = (nativeTelemetryDrainRoutineFor (constructor TelemetryDrainRoutineKind TelemetryDrainReadyRoutine)) -- ABI: publication arena, rendered-record arena, event bytes, exact publication -- extent, record extent. The caller's arena certificate supplies live disjoint -- buffers. Invalid publication extent refuses without touching its pointer; -- once accessible, any rejection clears readiness before a later seal. -- Success records the bounded destination and LF and advances the private byte -- cursor. The maintained memory-copy owner then copies the event bytes before -- the next iteration; no external reader can see this unsealed staging area. def drainAppendAssembly = (lambda unrestricted bound : Nat . (telemetryDrainAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) drainX86Backend (constructor TelemetryDrainRoutineKind TelemetryDrainAppendRoutine bound))) def drainAppendRoutine = (lambda unrestricted bound : Nat . (compiler-native-encode (family X86NativeAssembly) (drainAppendAssembly bound))) -- The canonical copy owner supplies exactly the bytes used by host twin -- lookup; avoid selecting a second equivalent encoding at this consumer. def drainMemoryCopyRoutine : Bytes = nativeMemoryCopyRoutineBytes def drainState = (lambda unrestricted offset : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated offset))) def drainStore = (lambda unrestricted offset : Nat . (lambda unrestricted value : (family NativePhysicalOperand) . (lambda unrestricted identity : Bytes . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 (drainState offset) value) identity)))) def drainRecordCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bound : Nat . (lambda unrestricted scratchBytes : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTelemetryRecordCommands recipe (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationSavedR13At) (drainState (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)) (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound) resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (drainAppendRoutine bound) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) (drainState (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound)) (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe)) (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound)) (nativeLaunchRecipeImmediate scratchBytes) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine drainMemoryCopyRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationSavedR12At) (drainState (naturalAdd (telemetryDrainScratchAt applicationBytes ordinaryCapacity reservedCapacity bound) telemetryRecordAt)) (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe)) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalAddWord64 (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity publicationSavedR13At) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationSavedR13At) (nativeLaunchRecipeImmediate captureRecordBytes)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail))))))))))))))) def drainOccupiedQueueWith = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted render : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted sourceAt : Nat . (lambda unrestricted occupiedAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (drainStore (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) publicationSavedR13At) (drainState sourceAt) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity (naturalAdd publicationBodyAt (naturalAdd nativeTelemetryCountersAt occupiedAt)))) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine drainReadyRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue resultSlot)) identity (render (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail)))))))))))))))) def drainQueueCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted sourceAt : Nat . (lambda unrestricted occupiedAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (aosChoose (family NativePhysicalCommands) (naturalNonzero (aosChoose Nat (naturalEqual occupiedAt captureOrdinaryUsedAt) ordinaryCapacity reservedCapacity)) (drainOccupiedQueueWith applicationBytes ordinaryCapacity reservedCapacity (drainRecordCommands applicationBytes ordinaryCapacity reservedCapacity bound (telemetryDrainScratchBytesForCapacities ordinaryCapacity reservedCapacity ordinary reserved) recipe resultSlot identity) sourceAt occupiedAt resultSlot identity tail) tail))))))))))))) -- Bounds are derived from the declared capacities/recipes, while actual byte -- lengths follow occupancy. An empty queue emits no event. Render refusal -- leaves all captures pending; a durable commit alone reclaims the queues. def drainPreparedWith = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinaryDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted reservedDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted descriptors : Bytes . (lambda unrestricted bound : Nat . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTelemetryPublicationPrepareCommandsForBody applicationBytes ordinaryCapacity reservedCapacity bound terminal resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationReadyAt)) identity (publicationCopyPayload applicationBytes ordinaryCapacity reservedCapacity (naturalAdd publicationBodyAt publicationPayloadRecordsAt) descriptors identity (drainStore (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) publicationBodyLengthAt) (nativeLaunchRecipeImmediate (naturalAdd publicationPayloadRecordsAt (bytes-length descriptors))) identity (drainStore (naturalAdd (publicationBase applicationBytes ordinaryCapacity reservedCapacity) (naturalAdd publicationBodyAt nativeTelemetryEmptyErrorPayloadExtentAt)) (nativeLaunchRecipeImmediate (naturalAdd captureWordBytes (bytes-length descriptors))) identity (ordinaryDrain (reservedDrain (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (nativeTelemetryPublicationTypedPaddingRoutineForBody bound) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound)) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity (naturalAdd publicationBodyAt nativeTelemetryEmptyErrorPayloadExtentAt)) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity (publicationSealAndCommitCommandsForBody applicationBytes ordinaryCapacity reservedCapacity bound sink directory resultSlot identity tail))))))))))))))))))))))) def drainPreparedCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted descriptors : Bytes . (lambda unrestricted bound : Nat . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (drainPreparedWith applicationBytes ordinaryCapacity reservedCapacity (drainQueueCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound ordinary (captureQueueAt applicationBytes) captureOrdinaryUsedAt resultSlot identity) (drainQueueCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound reserved (naturalAdd (captureQueueAt applicationBytes) (naturalMultiply ordinaryCapacity captureRecordBytes)) captureReservedUsedAt resultSlot identity) descriptors bound terminal sink directory resultSlot identity tail)))))))))))))) def nativeTelemetryDrainCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryDrainPlan) . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryDrainPlan (lambda unrestricted current : (family TelemetryDrainPlan) . (family NativePhysicalCommands)) plan (branch TelemetryDrainReady ordinaryCapacity reservedCapacity ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (telemetryDrainArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (drainPreparedCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved descriptors bound terminal sink directory resultSlot identity tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))) (branch TelemetryDrainRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))))))))))) -- Route metadata is committed immediately after the shared capture primitive. -- Publication cannot run between those commands. An unexpected tag failure -- leaves an unroutable capture queued, never a falsely acknowledged event. def drainCommitTagRoutine = (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted role : Nat . (lambda unrestricted tag : Nat . (nativeTelemetryDrainRoutineFor (constructor TelemetryDrainRoutineKind TelemetryDrainCommitTagRoutine ordinaryCapacity reservedCapacity role tag)))))) def drainReadTagRoutine = (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted routes : (family TelemetryRecordRoutes) . (nativeTelemetryDrainRoutineFor (constructor TelemetryDrainRoutineKind TelemetryDrainReadTagRoutine ordinaryCapacity reservedCapacity routes))))) def drainMatchTagRoutine = (lambda unrestricted tag : Nat . (nativeTelemetryDrainRoutineFor (constructor TelemetryDrainRoutineKind TelemetryDrainMatchTagRoutine tag))) def drainRenderRoutes = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted routes : (family TelemetryRecordRoutes) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (app (eliminate TelemetryRecordRoutes (lambda unrestricted current : (family TelemetryRecordRoutes) . (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands))) routes (branch TelemetryRecordRoutesEnd . (lambda unrestricted commands : (family NativePhysicalCommands) . commands)) (branch TelemetryRecordRoutesNext tag recipe following induction . (lambda unrestricted commands : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (drainMatchTagRoutine tag) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (drainState (telemetryDispatchTagScratchAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue resultSlot)) identity (drainRecordCommands applicationBytes ordinaryCapacity reservedCapacity bound (telemetryDrainScratchBytesForCapacities ordinaryCapacity reservedCapacity ordinary reserved) recipe resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity (induction commands)))))))) tail))))))))))) def drainDispatchRecordCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted routes : (family TelemetryRecordRoutes) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (drainReadTagRoutine ordinaryCapacity reservedCapacity routes) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (publicationStateAddress applicationBytes ordinaryCapacity reservedCapacity 0) (publicationStateLoad applicationBytes ordinaryCapacity reservedCapacity publicationSavedR13At) (drainState (captureQueueAt applicationBytes)) (drainState (telemetryDispatchTagsAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (nativeLaunchRecipeImmediate (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity)) (drainState (telemetryDispatchTagScratchAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound))) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue resultSlot)) identity (drainRenderRoutes applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound routes resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail)))))))))))))) def drainDispatchQueueCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted routes : (family TelemetryRecordRoutes) . (lambda unrestricted sourceAt : Nat . (lambda unrestricted occupiedAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (aosChoose (family NativePhysicalCommands) (naturalNonzero (aosChoose Nat (naturalEqual occupiedAt captureOrdinaryUsedAt) ordinaryCapacity reservedCapacity)) (drainOccupiedQueueWith applicationBytes ordinaryCapacity reservedCapacity (drainDispatchRecordCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound routes resultSlot identity) sourceAt occupiedAt resultSlot identity tail) tail))))))))))))) def nativeTelemetryDispatchDrainCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryDispatchPlan) . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativePhysicalCommands)) plan (branch TelemetryDispatchReady ordinaryCapacity reservedCapacity ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (telemetryDispatchArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (drainPreparedWith applicationBytes ordinaryCapacity reservedCapacity (drainDispatchQueueCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound ordinaryRoutes (captureQueueAt applicationBytes) captureOrdinaryUsedAt resultSlot identity) (drainDispatchQueueCommands applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound reservedRoutes (naturalAdd (captureQueueAt applicationBytes) (naturalMultiply ordinaryCapacity captureRecordBytes)) captureReservedUsedAt resultSlot identity) descriptors bound terminal sink directory resultSlot identity tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))) (branch TelemetryDispatchRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))))))))))) def nativeTelemetryDispatchCaptureCommand = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryDispatchPlan) . (lambda unrestricted selected : Nat . (lambda unrestricted role : Nat . (lambda unrestricted tag : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativePhysicalCommands)) plan (branch TelemetryDispatchReady ordinaryCapacity reservedCapacity ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (naturalAnd (naturalLessOrEqual role 1) (naturalAnd (naturalLessOrEqual selected 1) (naturalAnd (telemetryDispatchArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (telemetryRecordRouteContains tag (aosChoose (family TelemetryRecordRoutes) role reservedRoutes ordinaryRoutes))))) (nativeTelemetryCaptureCommand applicationBytes ordinaryCapacity reservedCapacity selected role resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (drainCommitTagRoutine ordinaryCapacity reservedCapacity role tag) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (drainState (captureControlAt applicationBytes)) (drainState (telemetryDispatchTagsAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity)) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))) (branch TelemetryDispatchRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))))))))))