1module Runtime.NativeTelemetryDrain
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeAssembly
5import Data.Bytes
6import Model.Word64
7import Observe.Value
8import Runtime.NativeLaunchRecipeLoad
9import Runtime.NativeMemoryRoutine
10import Runtime.NativePhysicalProgram
11import Runtime.NativeTelemetry
12import Runtime.NativeTelemetryCapture
13import Runtime.NativeTelemetryPublication
14import Runtime.NativeTelemetryRecord
15import Runtime.NativeTelemetrySeal
16import Runtime.TelemetryCapture
17import Runtime.TelemetryDrain
18import Runtime.TelemetryDrainRoutine
19import Runtime.TelemetryIdentity
20import Runtime.TelemetryPublication
21import Runtime.TelemetryRecord
22import Std.Natural
23import Runtime.NativeWordDigest
24
25-- System V realization of shared staging/tag semantics. Registers and
26-- instruction choices preserve the existing routine identities.
27def drainX86JumpIf =
28 (lambda unrestricted condition : (family TelemetryDrainCondition) .
29 (digestJumpIf
30 (eliminate
31 TelemetryDrainCondition
32 (lambda unrestricted current : (family TelemetryDrainCondition) .
33 (family X86NativeCondition))
34 condition
35 (branch TelemetryDrainZero . (constructor X86NativeCondition X86NativeConditionZero))
36 (branch TelemetryDrainNotZero . (constructor X86NativeCondition X86NativeConditionNotZero))
37 (branch TelemetryDrainBelow . (constructor X86NativeCondition X86NativeConditionBelow))
38 (branch TelemetryDrainAbove . (constructor X86NativeCondition X86NativeConditionAbove)))))
39
40def drainX86Divide =
41 (lambda unrestricted divisor : (family X86NativeRegister64) .
42 (digestEmit (constructor X86NativeInstruction X86NativeDivideRegister64Unsigned divisor)))
43
44def drainX86Backend =
45 (constructor
46 TelemetryDrainBackend
47 TelemetryDrainBackendValue
48 (family X86NativeAssembly)
49 (family X86NativeRegister64)
50 digestMovImm
51 digestMov
52 digestLoad64
53 digestStore64
54 digestStore8
55 digestCmpImm
56 publicationCompare
57 publicationSubtract
58 digestAdd
59 digestAddImm
60 digestMulImm
61 drainX86Divide
62 drainX86JumpIf
63 publicationJump
64 digestLabel
65 digestReturn
66 digestEnd
67 digestRAX
68 digestRDI
69 digestRSI
70 digestRDX
71 digestRCX
72 digestR8
73 digestR9
74 digestR10
75 digestR11)
76
77def nativeTelemetryDrainRoutineFor =
78 (lambda unrestricted kind : (family TelemetryDrainRoutineKind) .
79 (compiler-native-encode
80 (family X86NativeAssembly)
81 (telemetryDrainAssemblyFor
82 (family X86NativeAssembly)
83 (family X86NativeRegister64)
84 drainX86Backend
85 kind)))
86
87-- A single writer drains the occupied prefixes at a safe boundary. No record
88-- formatting occurs in acquisition. Source pointers advance only after a
89-- rendered record has passed append preflight and its bytes have been copied.
90-- Private saved-register cells are cursor scratch until the shared commit
91-- owner uses them; no commit or acquisition may run concurrently with a drain.
92def drainReadyAssembly : (family X86NativeAssembly) =
93 (telemetryDrainAssemblyFor
94 (family X86NativeAssembly)
95 (family X86NativeRegister64)
96 drainX86Backend
97 (constructor TelemetryDrainRoutineKind TelemetryDrainReadyRoutine))
98
99def drainReadyRoutine : Bytes =
100 (nativeTelemetryDrainRoutineFor
101 (constructor TelemetryDrainRoutineKind TelemetryDrainReadyRoutine))
102
103-- ABI: publication arena, rendered-record arena, event bytes, exact publication
104-- extent, record extent. The caller's arena certificate supplies live disjoint
105-- buffers. Invalid publication extent refuses without touching its pointer;
106-- once accessible, any rejection clears readiness before a later seal.
107-- Success records the bounded destination and LF and advances the private byte
108-- cursor. The maintained memory-copy owner then copies the event bytes before
109-- the next iteration; no external reader can see this unsealed staging area.
110def drainAppendAssembly =
111 (lambda unrestricted bound : Nat .
112 (telemetryDrainAssemblyFor
113 (family X86NativeAssembly)
114 (family X86NativeRegister64)
115 drainX86Backend
116 (constructor TelemetryDrainRoutineKind TelemetryDrainAppendRoutine bound)))
117
118def drainAppendRoutine =
119 (lambda unrestricted bound : Nat .
120 (compiler-native-encode (family X86NativeAssembly) (drainAppendAssembly bound)))
121
122-- The canonical copy owner supplies exactly the bytes used by host twin
123-- lookup; avoid selecting a second equivalent encoding at this consumer.
124def drainMemoryCopyRoutine : Bytes =
125 nativeMemoryCopyRoutineBytes
126
127def drainState =
128 (lambda unrestricted offset : Nat .
129 (constructor
130 NativePhysicalOperand
131 NativePhysicalStateAddress
132 (modelWord64FromNaturalTruncated offset)))
133
134def drainStore =
135 (lambda unrestricted offset : Nat .
136 (lambda unrestricted value : (family NativePhysicalOperand) .
137 (lambda unrestricted identity : Bytes .
138 (nativeLaunchRecipeCommand
139 (constructor NativePhysicalOperation NativePhysicalStoreWord64 (drainState offset) value)
140 identity))))
141
142def drainRecordCommands =
143 (lambda unrestricted applicationBytes : Nat .
144 (lambda unrestricted ordinaryCapacity : Nat .
145 (lambda unrestricted reservedCapacity : Nat .
146 (lambda unrestricted bound : Nat .
147 (lambda unrestricted scratchBytes : Nat .
148 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
149 (lambda unrestricted resultSlot : Nat .
150 (lambda unrestricted identity : Bytes .
151 (lambda unrestricted tail : (family NativePhysicalCommands) .
152 (nativeTelemetryRecordCommands
153 recipe
154 (publicationStateLoad
155 applicationBytes
156 ordinaryCapacity
157 reservedCapacity
158 publicationSavedR13At)
159 (drainState
160 (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity))
161 (telemetryDrainScratchAt
162 applicationBytes
163 ordinaryCapacity
164 reservedCapacity
165 bound)
166 resultSlot
167 identity
168 (nativeLaunchRecipeCommand
169 (constructor
170 NativePhysicalOperation
171 NativePhysicalMachineRoutine
172 (drainAppendRoutine bound)
173 (constructor
174 NativePhysicalArguments
175 NativePhysicalArgumentsValue
176 (publicationStateAddress
177 applicationBytes
178 ordinaryCapacity
179 reservedCapacity
180 0)
181 (drainState
182 (telemetryDrainScratchAt
183 applicationBytes
184 ordinaryCapacity
185 reservedCapacity
186 bound))
187 (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe))
188 (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound))
189 (nativeLaunchRecipeImmediate scratchBytes)
190 (nativeLaunchRecipeImmediate 0))
191 (nativeLaunchRecipeStore resultSlot))
192 identity
193 (nativeLaunchRecipeCommand
194 (constructor
195 NativePhysicalOperation
196 NativePhysicalRepeatBeginCounted
197 (nativeLaunchRecipeSlotValue resultSlot))
198 identity
199 (nativeLaunchRecipeCommand
200 (constructor
201 NativePhysicalOperation
202 NativePhysicalMachineRoutine
203 drainMemoryCopyRoutine
204 (constructor
205 NativePhysicalArguments
206 NativePhysicalArgumentsValue
207 (publicationStateLoad
208 applicationBytes
209 ordinaryCapacity
210 reservedCapacity
211 publicationSavedR12At)
212 (drainState
213 (naturalAdd
214 (telemetryDrainScratchAt
215 applicationBytes
216 ordinaryCapacity
217 reservedCapacity
218 bound)
219 telemetryRecordAt))
220 (nativeLaunchRecipeImmediate (telemetryDrainRecordBytes recipe))
221 (nativeLaunchRecipeImmediate 0)
222 (nativeLaunchRecipeImmediate 0)
223 (nativeLaunchRecipeImmediate 0))
224 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
225 identity
226 (nativeLaunchRecipeCommand
227 (constructor
228 NativePhysicalOperation
229 NativePhysicalAddWord64
230 (publicationStateAddress
231 applicationBytes
232 ordinaryCapacity
233 reservedCapacity
234 publicationSavedR13At)
235 (publicationStateLoad
236 applicationBytes
237 ordinaryCapacity
238 reservedCapacity
239 publicationSavedR13At)
240 (nativeLaunchRecipeImmediate captureRecordBytes))
241 identity
242 (nativeLaunchRecipeCommand
243 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
244 identity
245 tail)))))))))))))))
246
247def drainOccupiedQueueWith =
248 (lambda unrestricted applicationBytes : Nat .
249 (lambda unrestricted ordinaryCapacity : Nat .
250 (lambda unrestricted reservedCapacity : Nat .
251 (lambda unrestricted render : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
252 (lambda unrestricted sourceAt : Nat .
253 (lambda unrestricted occupiedAt : Nat .
254 (lambda unrestricted resultSlot : Nat .
255 (lambda unrestricted identity : Bytes .
256 (lambda unrestricted tail : (family NativePhysicalCommands) .
257 (drainStore
258 (naturalAdd
259 (publicationBase applicationBytes ordinaryCapacity reservedCapacity)
260 publicationSavedR13At)
261 (drainState sourceAt)
262 identity
263 (nativeLaunchRecipeCommand
264 (constructor
265 NativePhysicalOperation
266 NativePhysicalRepeatBeginCounted
267 (publicationStateLoad
268 applicationBytes
269 ordinaryCapacity
270 reservedCapacity
271 (naturalAdd
272 publicationBodyAt
273 (naturalAdd nativeTelemetryCountersAt occupiedAt))))
274 identity
275 (nativeLaunchRecipeCommand
276 (constructor
277 NativePhysicalOperation
278 NativePhysicalMachineRoutine
279 drainReadyRoutine
280 (constructor
281 NativePhysicalArguments
282 NativePhysicalArgumentsValue
283 (publicationStateAddress
284 applicationBytes
285 ordinaryCapacity
286 reservedCapacity
287 0)
288 (nativeLaunchRecipeImmediate 0)
289 (nativeLaunchRecipeImmediate 0)
290 (nativeLaunchRecipeImmediate 0)
291 (nativeLaunchRecipeImmediate 0)
292 (nativeLaunchRecipeImmediate 0))
293 (nativeLaunchRecipeStore resultSlot))
294 identity
295 (nativeLaunchRecipeCommand
296 (constructor
297 NativePhysicalOperation
298 NativePhysicalRepeatBeginCounted
299 (nativeLaunchRecipeSlotValue resultSlot))
300 identity
301 (render
302 (nativeLaunchRecipeCommand
303 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
304 identity
305 (nativeLaunchRecipeCommand
306 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
307 identity
308 tail))))))))))))))))
309
310def drainQueueCommands =
311 (lambda unrestricted applicationBytes : Nat .
312 (lambda unrestricted ordinaryCapacity : Nat .
313 (lambda unrestricted reservedCapacity : Nat .
314 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
315 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
316 (lambda unrestricted bound : Nat .
317 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
318 (lambda unrestricted sourceAt : Nat .
319 (lambda unrestricted occupiedAt : Nat .
320 (lambda unrestricted resultSlot : Nat .
321 (lambda unrestricted identity : Bytes .
322 (lambda unrestricted tail : (family NativePhysicalCommands) .
323 (aosChoose
324 (family NativePhysicalCommands)
325 (naturalNonzero
326 (aosChoose
327 Nat
328 (naturalEqual occupiedAt captureOrdinaryUsedAt)
329 ordinaryCapacity
330 reservedCapacity))
331 (drainOccupiedQueueWith
332 applicationBytes
333 ordinaryCapacity
334 reservedCapacity
335 (drainRecordCommands
336 applicationBytes
337 ordinaryCapacity
338 reservedCapacity
339 bound
340 (telemetryDrainScratchBytesForCapacities
341 ordinaryCapacity
342 reservedCapacity
343 ordinary
344 reserved)
345 recipe
346 resultSlot
347 identity)
348 sourceAt
349 occupiedAt
350 resultSlot
351 identity
352 tail)
353 tail)))))))))))))
354
355-- Bounds are derived from the declared capacities/recipes, while actual byte
356-- lengths follow occupancy. An empty queue emits no event. Render refusal
357-- leaves all captures pending; a durable commit alone reclaims the queues.
358def drainPreparedWith =
359 (lambda unrestricted applicationBytes : Nat .
360 (lambda unrestricted ordinaryCapacity : Nat .
361 (lambda unrestricted reservedCapacity : Nat .
362 (lambda unrestricted ordinaryDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
363 (lambda unrestricted reservedDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
364 (lambda unrestricted descriptors : Bytes .
365 (lambda unrestricted bound : Nat .
366 (lambda unrestricted terminal : Nat .
367 (lambda unrestricted sink : (family NativePhysicalOperand) .
368 (lambda unrestricted directory : (family NativePhysicalOperand) .
369 (lambda unrestricted resultSlot : Nat .
370 (lambda unrestricted identity : Bytes .
371 (lambda unrestricted tail : (family NativePhysicalCommands) .
372 (nativeTelemetryPublicationPrepareCommandsForBody
373 applicationBytes
374 ordinaryCapacity
375 reservedCapacity
376 bound
377 terminal
378 resultSlot
379 identity
380 (nativeLaunchRecipeCommand
381 (constructor
382 NativePhysicalOperation
383 NativePhysicalRepeatBeginCounted
384 (publicationStateLoad
385 applicationBytes
386 ordinaryCapacity
387 reservedCapacity
388 publicationReadyAt))
389 identity
390 (publicationCopyPayload
391 applicationBytes
392 ordinaryCapacity
393 reservedCapacity
394 (naturalAdd publicationBodyAt publicationPayloadRecordsAt)
395 descriptors
396 identity
397 (drainStore
398 (naturalAdd
399 (publicationBase
400 applicationBytes
401 ordinaryCapacity
402 reservedCapacity)
403 publicationBodyLengthAt)
404 (nativeLaunchRecipeImmediate
405 (naturalAdd
406 publicationPayloadRecordsAt
407 (bytes-length descriptors)))
408 identity
409 (drainStore
410 (naturalAdd
411 (publicationBase
412 applicationBytes
413 ordinaryCapacity
414 reservedCapacity)
415 (naturalAdd
416 publicationBodyAt
417 nativeTelemetryEmptyErrorPayloadExtentAt))
418 (nativeLaunchRecipeImmediate
419 (naturalAdd captureWordBytes (bytes-length descriptors)))
420 identity
421 (ordinaryDrain
422 (reservedDrain
423 (nativeLaunchRecipeCommand
424 (constructor
425 NativePhysicalOperation
426 NativePhysicalMachineRoutine
427 (nativeTelemetryPublicationTypedPaddingRoutineForBody bound)
428 (constructor
429 NativePhysicalArguments
430 NativePhysicalArgumentsValue
431 (publicationStateAddress
432 applicationBytes
433 ordinaryCapacity
434 reservedCapacity
435 0)
436 (nativeLaunchRecipeImmediate
437 (publicationArenaBytesForBody bound))
438 (publicationStateLoad
439 applicationBytes
440 ordinaryCapacity
441 reservedCapacity
442 (naturalAdd
443 publicationBodyAt
444 nativeTelemetryEmptyErrorPayloadExtentAt))
445 (nativeLaunchRecipeImmediate 0)
446 (nativeLaunchRecipeImmediate 0)
447 (nativeLaunchRecipeImmediate 0))
448 (nativeLaunchRecipeStore resultSlot))
449 identity
450 (nativeLaunchRecipeCommand
451 (constructor
452 NativePhysicalOperation
453 NativePhysicalRepeatEnd)
454 identity
455 (publicationSealAndCommitCommandsForBody
456 applicationBytes
457 ordinaryCapacity
458 reservedCapacity
459 bound
460 sink
461 directory
462 resultSlot
463 identity
464 tail)))))))))))))))))))))))
465
466def drainPreparedCommands =
467 (lambda unrestricted applicationBytes : Nat .
468 (lambda unrestricted ordinaryCapacity : Nat .
469 (lambda unrestricted reservedCapacity : Nat .
470 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
471 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
472 (lambda unrestricted descriptors : Bytes .
473 (lambda unrestricted bound : Nat .
474 (lambda unrestricted terminal : Nat .
475 (lambda unrestricted sink : (family NativePhysicalOperand) .
476 (lambda unrestricted directory : (family NativePhysicalOperand) .
477 (lambda unrestricted resultSlot : Nat .
478 (lambda unrestricted identity : Bytes .
479 (lambda unrestricted tail : (family NativePhysicalCommands) .
480 (drainPreparedWith
481 applicationBytes
482 ordinaryCapacity
483 reservedCapacity
484 (drainQueueCommands
485 applicationBytes
486 ordinaryCapacity
487 reservedCapacity
488 ordinary
489 reserved
490 bound
491 ordinary
492 (captureQueueAt applicationBytes)
493 captureOrdinaryUsedAt
494 resultSlot
495 identity)
496 (drainQueueCommands
497 applicationBytes
498 ordinaryCapacity
499 reservedCapacity
500 ordinary
501 reserved
502 bound
503 reserved
504 (naturalAdd
505 (captureQueueAt applicationBytes)
506 (naturalMultiply ordinaryCapacity captureRecordBytes))
507 captureReservedUsedAt
508 resultSlot
509 identity)
510 descriptors
511 bound
512 terminal
513 sink
514 directory
515 resultSlot
516 identity
517 tail))))))))))))))
518
519def nativeTelemetryDrainCommands =
520 (lambda unrestricted applicationBytes : Nat .
521 (lambda unrestricted plan : (family TelemetryDrainPlan) .
522 (lambda unrestricted terminal : Nat .
523 (lambda unrestricted sink : (family NativePhysicalOperand) .
524 (lambda unrestricted directory : (family NativePhysicalOperand) .
525 (lambda unrestricted resultSlot : Nat .
526 (lambda unrestricted identity : Bytes .
527 (lambda unrestricted tail : (family NativePhysicalCommands) .
528 (eliminate
529 TelemetryDrainPlan
530 (lambda unrestricted current : (family TelemetryDrainPlan) .
531 (family NativePhysicalCommands))
532 plan
533 (branch
534 TelemetryDrainReady
535 ordinaryCapacity
536 reservedCapacity
537 ordinary
538 reserved
539 descriptors
540 bound
541 .
542 (aosChoose
543 (family NativePhysicalCommands)
544 (telemetryDrainArenaCertificate
545 applicationBytes
546 ordinaryCapacity
547 reservedCapacity
548 ordinary
549 reserved
550 bound)
551 (drainPreparedCommands
552 applicationBytes
553 ordinaryCapacity
554 reservedCapacity
555 ordinary
556 reserved
557 descriptors
558 bound
559 terminal
560 sink
561 directory
562 resultSlot
563 identity
564 tail)
565 (nativeLaunchRecipeCommand
566 (constructor
567 NativePhysicalOperation
568 NativePhysicalMachineRoutine
569 b""
570 (nativeLaunchRecipeArguments
571 (nativeLaunchRecipeImmediate 0)
572 (nativeLaunchRecipeImmediate 0)
573 (nativeLaunchRecipeImmediate 0)
574 (nativeLaunchRecipeImmediate 0))
575 (nativeLaunchRecipeStore resultSlot))
576 identity
577 tail)))
578 (branch
579 TelemetryDrainRefused
580 reason
581 .
582 (nativeLaunchRecipeCommand
583 (constructor
584 NativePhysicalOperation
585 NativePhysicalMachineRoutine
586 b""
587 (nativeLaunchRecipeArguments
588 (nativeLaunchRecipeImmediate 0)
589 (nativeLaunchRecipeImmediate 0)
590 (nativeLaunchRecipeImmediate 0)
591 (nativeLaunchRecipeImmediate 0))
592 (nativeLaunchRecipeStore resultSlot))
593 identity
594 tail)))))))))))
595
596-- Route metadata is committed immediately after the shared capture primitive.
597-- Publication cannot run between those commands. An unexpected tag failure
598-- leaves an unroutable capture queued, never a falsely acknowledged event.
599def drainCommitTagRoutine =
600 (lambda unrestricted ordinaryCapacity : Nat .
601 (lambda unrestricted reservedCapacity : Nat .
602 (lambda unrestricted role : Nat .
603 (lambda unrestricted tag : Nat .
604 (nativeTelemetryDrainRoutineFor
605 (constructor
606 TelemetryDrainRoutineKind
607 TelemetryDrainCommitTagRoutine
608 ordinaryCapacity
609 reservedCapacity
610 role
611 tag))))))
612
613def drainReadTagRoutine =
614 (lambda unrestricted ordinaryCapacity : Nat .
615 (lambda unrestricted reservedCapacity : Nat .
616 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
617 (nativeTelemetryDrainRoutineFor
618 (constructor
619 TelemetryDrainRoutineKind
620 TelemetryDrainReadTagRoutine
621 ordinaryCapacity
622 reservedCapacity
623 routes)))))
624
625def drainMatchTagRoutine =
626 (lambda unrestricted tag : Nat .
627 (nativeTelemetryDrainRoutineFor
628 (constructor TelemetryDrainRoutineKind TelemetryDrainMatchTagRoutine tag)))
629
630def drainRenderRoutes =
631 (lambda unrestricted applicationBytes : Nat .
632 (lambda unrestricted ordinaryCapacity : Nat .
633 (lambda unrestricted reservedCapacity : Nat .
634 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
635 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
636 (lambda unrestricted bound : Nat .
637 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
638 (lambda unrestricted resultSlot : Nat .
639 (lambda unrestricted identity : Bytes .
640 (lambda unrestricted tail : (family NativePhysicalCommands) .
641 (app
642 (eliminate
643 TelemetryRecordRoutes
644 (lambda unrestricted current : (family TelemetryRecordRoutes) .
645 (pi unrestricted commands : (family NativePhysicalCommands) .
646 (family NativePhysicalCommands)))
647 routes
648 (branch
649 TelemetryRecordRoutesEnd
650 .
651 (lambda unrestricted commands : (family NativePhysicalCommands) .
652 commands))
653 (branch
654 TelemetryRecordRoutesNext
655 tag
656 recipe
657 following
658 induction
659 .
660 (lambda unrestricted commands : (family NativePhysicalCommands) .
661 (nativeLaunchRecipeCommand
662 (constructor
663 NativePhysicalOperation
664 NativePhysicalMachineRoutine
665 (drainMatchTagRoutine tag)
666 (constructor
667 NativePhysicalArguments
668 NativePhysicalArgumentsValue
669 (drainState
670 (telemetryDispatchTagScratchAt
671 applicationBytes
672 ordinaryCapacity
673 reservedCapacity
674 ordinary
675 reserved
676 bound))
677 (nativeLaunchRecipeImmediate 0)
678 (nativeLaunchRecipeImmediate 0)
679 (nativeLaunchRecipeImmediate 0)
680 (nativeLaunchRecipeImmediate 0)
681 (nativeLaunchRecipeImmediate 0))
682 (nativeLaunchRecipeStore resultSlot))
683 identity
684 (nativeLaunchRecipeCommand
685 (constructor
686 NativePhysicalOperation
687 NativePhysicalRepeatBeginCounted
688 (nativeLaunchRecipeSlotValue resultSlot))
689 identity
690 (drainRecordCommands
691 applicationBytes
692 ordinaryCapacity
693 reservedCapacity
694 bound
695 (telemetryDrainScratchBytesForCapacities
696 ordinaryCapacity
697 reservedCapacity
698 ordinary
699 reserved)
700 recipe
701 resultSlot
702 identity
703 (nativeLaunchRecipeCommand
704 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
705 identity
706 (induction commands))))))))
707 tail)))))))))))
708
709def drainDispatchRecordCommands =
710 (lambda unrestricted applicationBytes : Nat .
711 (lambda unrestricted ordinaryCapacity : Nat .
712 (lambda unrestricted reservedCapacity : Nat .
713 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
714 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
715 (lambda unrestricted bound : Nat .
716 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
717 (lambda unrestricted resultSlot : Nat .
718 (lambda unrestricted identity : Bytes .
719 (lambda unrestricted tail : (family NativePhysicalCommands) .
720 (nativeLaunchRecipeCommand
721 (constructor
722 NativePhysicalOperation
723 NativePhysicalMachineRoutine
724 (drainReadTagRoutine ordinaryCapacity reservedCapacity routes)
725 (constructor
726 NativePhysicalArguments
727 NativePhysicalArgumentsValue
728 (publicationStateAddress
729 applicationBytes
730 ordinaryCapacity
731 reservedCapacity
732 0)
733 (publicationStateLoad
734 applicationBytes
735 ordinaryCapacity
736 reservedCapacity
737 publicationSavedR13At)
738 (drainState (captureQueueAt applicationBytes))
739 (drainState
740 (telemetryDispatchTagsAt
741 applicationBytes
742 ordinaryCapacity
743 reservedCapacity
744 ordinary
745 reserved
746 bound))
747 (nativeLaunchRecipeImmediate
748 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity))
749 (drainState
750 (telemetryDispatchTagScratchAt
751 applicationBytes
752 ordinaryCapacity
753 reservedCapacity
754 ordinary
755 reserved
756 bound)))
757 (nativeLaunchRecipeStore resultSlot))
758 identity
759 (nativeLaunchRecipeCommand
760 (constructor
761 NativePhysicalOperation
762 NativePhysicalRepeatBeginCounted
763 (nativeLaunchRecipeSlotValue resultSlot))
764 identity
765 (drainRenderRoutes
766 applicationBytes
767 ordinaryCapacity
768 reservedCapacity
769 ordinary
770 reserved
771 bound
772 routes
773 resultSlot
774 identity
775 (nativeLaunchRecipeCommand
776 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
777 identity
778 tail))))))))))))))
779
780def drainDispatchQueueCommands =
781 (lambda unrestricted applicationBytes : Nat .
782 (lambda unrestricted ordinaryCapacity : Nat .
783 (lambda unrestricted reservedCapacity : Nat .
784 (lambda unrestricted ordinary : (family TelemetryRecordPlan) .
785 (lambda unrestricted reserved : (family TelemetryRecordPlan) .
786 (lambda unrestricted bound : Nat .
787 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
788 (lambda unrestricted sourceAt : Nat .
789 (lambda unrestricted occupiedAt : Nat .
790 (lambda unrestricted resultSlot : Nat .
791 (lambda unrestricted identity : Bytes .
792 (lambda unrestricted tail : (family NativePhysicalCommands) .
793 (aosChoose
794 (family NativePhysicalCommands)
795 (naturalNonzero
796 (aosChoose
797 Nat
798 (naturalEqual occupiedAt captureOrdinaryUsedAt)
799 ordinaryCapacity
800 reservedCapacity))
801 (drainOccupiedQueueWith
802 applicationBytes
803 ordinaryCapacity
804 reservedCapacity
805 (drainDispatchRecordCommands
806 applicationBytes
807 ordinaryCapacity
808 reservedCapacity
809 ordinary
810 reserved
811 bound
812 routes
813 resultSlot
814 identity)
815 sourceAt
816 occupiedAt
817 resultSlot
818 identity
819 tail)
820 tail)))))))))))))
821
822def nativeTelemetryDispatchDrainCommands =
823 (lambda unrestricted applicationBytes : Nat .
824 (lambda unrestricted plan : (family TelemetryDispatchPlan) .
825 (lambda unrestricted terminal : Nat .
826 (lambda unrestricted sink : (family NativePhysicalOperand) .
827 (lambda unrestricted directory : (family NativePhysicalOperand) .
828 (lambda unrestricted resultSlot : Nat .
829 (lambda unrestricted identity : Bytes .
830 (lambda unrestricted tail : (family NativePhysicalCommands) .
831 (eliminate
832 TelemetryDispatchPlan
833 (lambda unrestricted current : (family TelemetryDispatchPlan) .
834 (family NativePhysicalCommands))
835 plan
836 (branch
837 TelemetryDispatchReady
838 ordinaryCapacity
839 reservedCapacity
840 ordinaryRoutes
841 reservedRoutes
842 ordinary
843 reserved
844 descriptors
845 bound
846 .
847 (aosChoose
848 (family NativePhysicalCommands)
849 (telemetryDispatchArenaCertificate
850 applicationBytes
851 ordinaryCapacity
852 reservedCapacity
853 ordinary
854 reserved
855 bound)
856 (drainPreparedWith
857 applicationBytes
858 ordinaryCapacity
859 reservedCapacity
860 (drainDispatchQueueCommands
861 applicationBytes
862 ordinaryCapacity
863 reservedCapacity
864 ordinary
865 reserved
866 bound
867 ordinaryRoutes
868 (captureQueueAt applicationBytes)
869 captureOrdinaryUsedAt
870 resultSlot
871 identity)
872 (drainDispatchQueueCommands
873 applicationBytes
874 ordinaryCapacity
875 reservedCapacity
876 ordinary
877 reserved
878 bound
879 reservedRoutes
880 (naturalAdd
881 (captureQueueAt applicationBytes)
882 (naturalMultiply ordinaryCapacity captureRecordBytes))
883 captureReservedUsedAt
884 resultSlot
885 identity)
886 descriptors
887 bound
888 terminal
889 sink
890 directory
891 resultSlot
892 identity
893 tail)
894 (nativeLaunchRecipeCommand
895 (constructor
896 NativePhysicalOperation
897 NativePhysicalMachineRoutine
898 b""
899 (constructor
900 NativePhysicalArguments
901 NativePhysicalArgumentsValue
902 (nativeLaunchRecipeImmediate 0)
903 (nativeLaunchRecipeImmediate 0)
904 (nativeLaunchRecipeImmediate 0)
905 (nativeLaunchRecipeImmediate 0)
906 (nativeLaunchRecipeImmediate 0)
907 (nativeLaunchRecipeImmediate 0))
908 (nativeLaunchRecipeStore resultSlot))
909 identity
910 tail)))
911 (branch
912 TelemetryDispatchRefused
913 reason
914 .
915 (nativeLaunchRecipeCommand
916 (constructor
917 NativePhysicalOperation
918 NativePhysicalMachineRoutine
919 b""
920 (constructor
921 NativePhysicalArguments
922 NativePhysicalArgumentsValue
923 (nativeLaunchRecipeImmediate 0)
924 (nativeLaunchRecipeImmediate 0)
925 (nativeLaunchRecipeImmediate 0)
926 (nativeLaunchRecipeImmediate 0)
927 (nativeLaunchRecipeImmediate 0)
928 (nativeLaunchRecipeImmediate 0))
929 (nativeLaunchRecipeStore resultSlot))
930 identity
931 tail)))))))))))
932
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.