1module Runtime.TelemetryPublicationRoutine
2
3import Data.Bytes
4import Observe.Value
5import Runtime.NativeTelemetry
6import Runtime.TelemetryCapture
7import Runtime.TelemetryIdentity
8import Runtime.TelemetryPublication
9import Std.Natural
10
11-- One single-writer snapshot, padding and durable-commit algorithm. Loads and
12-- stores retain little-endian wire words. Set retains 32 bits; CompareImmediate
13-- and AddImmediate sign-extend 32 bits. AddImmediate supplies Zero iff its full
14-- wrapped result is zero, including countdown loops. Comparisons are unsigned;
15-- branches preserve flags. Other arithmetic flags are not consumed.
16-- Write and Sync return the exact signed syscall result in Result and may
17-- clobber Argument0, Argument3 and Scratch1; other roles stay live. Argument3
18-- accounts for x86 syscall's RCX clobber. Commit saves Persistent0..3 in the
19-- caller's publication arena and restores them on every return.
20-- Full write, file sync AND containing-directory sync precede frontier advance
21-- and queue reclamation. Failed/short writes or sync poison the sink and retain
22-- every capture. Preparation/padding alone grant no durability or JSON meaning.
23family TelemetryPublicationCondition : Type 0
24constructor TelemetryPublicationZero
25constructor TelemetryPublicationNotZero
26constructor TelemetryPublicationBelow
27constructor TelemetryPublicationAbove
28
29end-family
30
31family TelemetryPublicationRoutineKind : Type 0
32constructor TelemetryPublicationPrepareRoutine
33field unrestricted publicationRoutineOrdinary : Nat
34field unrestricted publicationRoutineReserved : Nat
35field unrestricted publicationRoutineBodyBound : Nat
36constructor TelemetryPublicationTypedPaddingRoutine
37field unrestricted publicationRoutineTypedBodyBound : Nat
38constructor TelemetryPublicationCommitRoutine
39
40end-family
41
42family TelemetryPublicationBackend : Type 0
43parameter erased A : Type 0
44parameter erased R : Type 0
45constructor TelemetryPublicationBackendValue
46field unrestricted backendPubSet : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
47field unrestricted backendPubMove : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
48field unrestricted backendPubLoad64 : (pi unrestricted destination : R . (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted tail : A . A))))
49field unrestricted backendPubStore64 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A))))
50field unrestricted backendPubStore8 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A))))
51field unrestricted backendPubCompareImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
52field unrestricted backendPubCompare : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
53field unrestricted backendPubSubtract : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
54field unrestricted backendPubOr : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
55field unrestricted backendPubAdd : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
56field unrestricted backendPubAddImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
57field unrestricted backendPubMultiplyImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
58field unrestricted backendPubShiftRight : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
59field unrestricted backendPubJumpIf : (pi unrestricted condition : (family TelemetryPublicationCondition) . (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)))
60field unrestricted backendPubJump : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
61field unrestricted backendPubLabel : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
62field unrestricted backendPubReturn : (pi unrestricted tail : A . A)
63field unrestricted backendPubWrite : (pi unrestricted tail : A . A)
64field unrestricted backendPubSync : (pi unrestricted tail : A . A)
65field unrestricted backendPubEnd : A
66field unrestricted backendPubResult : R
67field unrestricted backendPubArgument0 : R
68field unrestricted backendPubArgument1 : R
69field unrestricted backendPubArgument2 : R
70field unrestricted backendPubArgument3 : R
71field unrestricted backendPubArgument4 : R
72field unrestricted backendPubArgument5 : R
73field unrestricted backendPubScratch0 : R
74field unrestricted backendPubScratch1 : R
75field unrestricted backendPubPersistent0 : R
76field unrestricted backendPubPersistent1 : R
77field unrestricted backendPubPersistent2 : R
78field unrestricted backendPubPersistent3 : R
79
80end-family
81
82def telemetryPublicationAssemblyFor =
83 (lambda erased A : Type 0 .
84 (lambda erased R : Type 0 .
85 (lambda unrestricted backend : (family TelemetryPublicationBackend A R) .
86 (lambda unrestricted kind : (family TelemetryPublicationRoutineKind) .
87 (eliminate
88 TelemetryPublicationBackend
89 (lambda unrestricted current : (family TelemetryPublicationBackend A R) . A)
90 backend
91 (branch
92 TelemetryPublicationBackendValue
93 pubSet
94 pubMove
95 pubLoad64
96 pubStore64
97 pubStore8
98 pubCompareImmediate
99 pubCompare
100 pubSubtract
101 pubOr
102 pubAdd
103 pubAddImmediate
104 pubMultiplyImmediate
105 pubShiftRight
106 pubJumpIf
107 pubJump
108 pubLabel
109 pubReturn
110 pubWrite
111 pubSync
112 pubEnd
113 pubResult
114 pubArgument0
115 pubArgument1
116 pubArgument2
117 pubArgument3
118 pubArgument4
119 pubArgument5
120 pubScratch0
121 pubScratch1
122 pubPersistent0
123 pubPersistent1
124 pubPersistent2
125 pubPersistent3
126 .
127 (let unrestricted publicationReturn =
128 (lambda unrestricted code : Nat .
129 (lambda unrestricted tail : A . (pubSet pubResult code (pubReturn tail))))
130 in
131 (let unrestricted publicationValidateOccupiedSequences =
132 (lambda unrestricted ordinaryCapacity : Nat .
133 (lambda unrestricted tail : A .
134 (pubStore64
135 pubArgument3
136 publicationSavedR12At
137 pubArgument0
138 (pubLoad64
139 pubScratch0
140 pubArgument0
141 captureOrdinaryUsedAt
142 (pubLoad64
143 pubScratch1
144 pubArgument0
145 captureReservedUsedAt
146 (pubMove
147 pubArgument4
148 pubArgument1
149 (pubMove
150 pubArgument5
151 pubArgument1
152 (pubAddImmediate
153 pubArgument5
154 (naturalMultiply ordinaryCapacity captureRecordBytes)
155 (pubLoad64
156 pubArgument2
157 pubArgument3
158 publicationPublishedNextAt
159 (pubLabel
160 b"publication-sequence-heads"
161 (pubCompareImmediate
162 pubScratch0
163 0
164 (pubJumpIf
165 (constructor
166 TelemetryPublicationCondition
167 TelemetryPublicationZero)
168 b"publication-sequence-reserved"
169 (pubCompareImmediate
170 pubScratch1
171 0
172 (pubJumpIf
173 (constructor
174 TelemetryPublicationCondition
175 TelemetryPublicationZero)
176 b"publication-sequence-ordinary"
177 (pubLoad64
178 pubResult
179 pubArgument4
180 captureSequenceAt
181 (pubLoad64
182 pubArgument0
183 pubArgument5
184 captureSequenceAt
185 (pubCompare
186 pubResult
187 pubArgument0
188 (pubJumpIf
189 (constructor
190 TelemetryPublicationCondition
191 TelemetryPublicationAbove)
192 b"publication-sequence-reserved"
193 (pubLabel
194 b"publication-sequence-ordinary"
195 (pubLoad64
196 pubResult
197 pubArgument4
198 captureSequenceAt
199 (pubAddImmediate
200 pubArgument4
201 captureRecordBytes
202 (pubAddImmediate
203 pubScratch0
204 0xffffffff
205 (pubJump
206 b"publication-sequence-check"
207 (pubLabel
208 b"publication-sequence-reserved"
209 (pubCompareImmediate
210 pubScratch1
211 0
212 (pubJumpIf
213 (constructor
214 TelemetryPublicationCondition
215 TelemetryPublicationZero)
216 b"publication-sequence-done"
217 (pubLoad64
218 pubResult
219 pubArgument5
220 captureSequenceAt
221 (pubAddImmediate
222 pubArgument5
223 captureRecordBytes
224 (pubAddImmediate
225 pubScratch1
226 0xffffffff
227 (pubLabel
228 b"publication-sequence-check"
229 (pubCompare
230 pubResult
231 pubArgument2
232 (pubJumpIf
233 (constructor
234 TelemetryPublicationCondition
235 TelemetryPublicationBelow)
236 b"publication-prepare-reject"
237 (pubLoad64
238 pubArgument0
239 pubArgument3
240 (naturalAdd
241 publicationBodyAt
242 (naturalAdd nativeTelemetryCountersAt captureNextSequenceAt))
243 (pubCompare
244 pubResult
245 pubArgument0
246 (pubJumpIf
247 (constructor
248 TelemetryPublicationCondition
249 TelemetryPublicationAbove)
250 b"publication-prepare-reject"
251 (pubJumpIf
252 (constructor
253 TelemetryPublicationCondition
254 TelemetryPublicationZero)
255 b"publication-prepare-reject"
256 (pubMove
257 pubArgument2
258 pubResult
259 (pubAddImmediate
260 pubArgument2
261 1
262 (pubJump
263 b"publication-sequence-heads"
264 (pubLabel
265 b"publication-sequence-done"
266 (pubLoad64
267 pubArgument0
268 pubArgument3
269 publicationSavedR12At
270 tail)))))))))))))))))))))))))))))))))))))))))
271 in
272 (let unrestricted publicationPreparePadding =
273 (pubLoad64
274 pubResult
275 pubArgument3
276 publicationBodyLengthAt
277 (pubMultiplyImmediate
278 pubResult
279 8
280 (pubShiftRight
281 pubResult
282 48
283 (pubStore8
284 pubScratch1
285 1
286 pubResult
287 (pubLoad64
288 pubResult
289 pubArgument3
290 publicationBodyLengthAt
291 (pubMultiplyImmediate
292 pubResult
293 8
294 (pubShiftRight
295 pubResult
296 40
297 (pubStore8
298 pubScratch1
299 2
300 pubResult
301 (pubLoad64
302 pubResult
303 pubArgument3
304 publicationBodyLengthAt
305 (pubMultiplyImmediate
306 pubResult
307 8
308 (pubShiftRight
309 pubResult
310 32
311 (pubStore8
312 pubScratch1
313 3
314 pubResult
315 (pubLoad64
316 pubResult
317 pubArgument3
318 publicationBodyLengthAt
319 (pubMultiplyImmediate
320 pubResult
321 8
322 (pubShiftRight
323 pubResult
324 24
325 (pubStore8
326 pubScratch1
327 4
328 pubResult
329 (pubLoad64
330 pubResult
331 pubArgument3
332 publicationBodyLengthAt
333 (pubMultiplyImmediate
334 pubResult
335 8
336 (pubShiftRight
337 pubResult
338 16
339 (pubStore8
340 pubScratch1
341 5
342 pubResult
343 (pubLoad64
344 pubResult
345 pubArgument3
346 publicationBodyLengthAt
347 (pubMultiplyImmediate
348 pubResult
349 8
350 (pubShiftRight
351 pubResult
352 8
353 (pubStore8
354 pubScratch1
355 6
356 pubResult
357 (pubLoad64
358 pubResult
359 pubArgument3
360 publicationBodyLengthAt
361 (pubMultiplyImmediate
362 pubResult
363 8
364 (pubStore8
365 pubScratch1
366 7
367 pubResult
368 (pubSet
369 pubResult
370 1
371 (pubStore64
372 pubArgument3
373 publicationReadyAt
374 pubResult
375 (publicationReturn
376 0
377 (pubLabel
378 b"publication-prepare-reject"
379 (publicationReturn 4 pubEnd))))))))))))))))))))))))))))))))
380 in
381 (let unrestricted publicationPadPreparedBody =
382 (pubSet
383 pubResult
384 128
385 (pubStore8
386 pubScratch1
387 0
388 pubResult
389 (pubAddImmediate
390 pubScratch1
391 1
392 (pubLoad64
393 pubScratch0
394 pubArgument3
395 publicationBlockCountAt
396 (pubMultiplyImmediate
397 pubScratch0
398 64
399 (pubLoad64
400 pubResult
401 pubArgument3
402 publicationBodyLengthAt
403 (pubSubtract
404 pubScratch0
405 pubResult
406 (pubAddImmediate
407 pubScratch0
408 (naturalSaturatingSubtract
409 4294967296
410 (naturalAdd 1 nativeTelemetryScalarBytes))
411 (pubCompareImmediate
412 pubScratch0
413 0
414 (pubJumpIf
415 (constructor
416 TelemetryPublicationCondition
417 TelemetryPublicationZero)
418 b"publication-length"
419 (pubSet
420 pubResult
421 0
422 (pubLabel
423 b"publication-zero-pad"
424 (pubStore8
425 pubScratch1
426 0
427 pubResult
428 (pubAddImmediate
429 pubScratch1
430 1
431 (pubAddImmediate
432 pubScratch0
433 0xffffffff
434 (pubJumpIf
435 (constructor
436 TelemetryPublicationCondition
437 TelemetryPublicationNotZero)
438 b"publication-zero-pad"
439 (pubLabel
440 b"publication-length"
441 (pubLoad64
442 pubResult
443 pubArgument3
444 publicationBodyLengthAt
445 (pubMultiplyImmediate
446 pubResult
447 8
448 (pubShiftRight
449 pubResult
450 56
451 (pubStore8
452 pubScratch1
453 0
454 pubResult
455 publicationPreparePadding)))))))))))))))))))))
456 in
457 (let unrestricted publicationPrepareOccupiedRecords =
458 (lambda unrestricted ordinaryCapacity : Nat .
459 (lambda unrestricted reservedCapacity : Nat .
460 (pubMove
461 pubArgument1
462 pubArgument4
463 (pubAddImmediate
464 pubArgument1
465 (naturalMultiply ordinaryCapacity captureRecordBytes)
466 (pubLoad64
467 pubScratch0
468 pubArgument0
469 captureReservedUsedAt
470 (pubMultiplyImmediate
471 pubScratch0
472 (naturalDivideUnchecked captureRecordBytes captureWordBytes)
473 (pubCompareImmediate
474 pubScratch0
475 0
476 (pubJumpIf
477 (constructor
478 TelemetryPublicationCondition
479 TelemetryPublicationZero)
480 b"publication-padding"
481 (pubLabel
482 b"publication-reserved-loop"
483 (pubLoad64
484 pubResult
485 pubArgument1
486 0
487 (pubStore64
488 pubScratch1
489 0
490 pubResult
491 (pubAddImmediate
492 pubArgument1
493 captureWordBytes
494 (pubAddImmediate
495 pubScratch1
496 captureWordBytes
497 (pubAddImmediate
498 pubScratch0
499 0xffffffff
500 (pubJumpIf
501 (constructor
502 TelemetryPublicationCondition
503 TelemetryPublicationNotZero)
504 b"publication-reserved-loop"
505 (pubLabel b"publication-padding" publicationPadPreparedBody))))))))))))))))
506 in
507 (let unrestricted publicationPrepareExtent =
508 (lambda unrestricted ordinaryCapacity : Nat .
509 (lambda unrestricted reservedCapacity : Nat .
510 (pubLoad64
511 pubResult
512 pubArgument2
513 (naturalMultiply 6 captureWordBytes)
514 (pubStore64
515 pubArgument3
516 (naturalAdd
517 publicationBodyAt
518 (naturalAdd
519 nativeTelemetryIdentityAt
520 (naturalMultiply 6 captureWordBytes)))
521 pubResult
522 (pubLoad64
523 pubResult
524 pubArgument0
525 (naturalMultiply 7 captureWordBytes)
526 (pubStore64
527 pubArgument3
528 (naturalAdd
529 publicationBodyAt
530 (naturalAdd
531 nativeTelemetryCountersAt
532 (naturalMultiply 7 captureWordBytes)))
533 pubResult
534 (pubLoad64
535 pubResult
536 pubArgument2
537 (naturalMultiply 7 captureWordBytes)
538 (pubStore64
539 pubArgument3
540 (naturalAdd
541 publicationBodyAt
542 (naturalAdd
543 nativeTelemetryIdentityAt
544 (naturalMultiply 7 captureWordBytes)))
545 pubResult
546 (pubLoad64
547 pubResult
548 pubArgument0
549 captureOrdinaryUsedAt
550 (pubLoad64
551 pubScratch0
552 pubArgument0
553 captureReservedUsedAt
554 (pubAdd
555 pubResult
556 pubScratch0
557 (pubMultiplyImmediate
558 pubResult
559 captureRecordBytes
560 (pubAddImmediate
561 pubResult
562 captureWordBytes
563 (pubStore64
564 pubArgument3
565 (naturalAdd
566 publicationBodyAt
567 nativeTelemetryEmptyErrorPayloadExtentAt)
568 pubResult
569 (pubAddImmediate
570 pubResult
571 nativeTelemetryEmptyErrorPayloadAt
572 (pubStore64
573 pubArgument3
574 publicationBodyLengthAt
575 pubResult
576 (pubAddImmediate
577 pubResult
578 (naturalAdd
579 1
580 (naturalAdd
581 nativeTelemetryScalarBytes
582 (naturalSaturatingSubtract 64 1)))
583 (pubShiftRight
584 pubResult
585 6
586 (pubStore64
587 pubArgument3
588 publicationBlockCountAt
589 pubResult
590 (pubLoad64
591 pubResult
592 pubArgument3
593 publicationBodyLengthAt
594 (pubAddImmediate
595 pubResult
596 (naturalAdd
597 (bytes-length nativeTelemetryMagic)
598 nativeTelemetryDigestBytes)
599 (pubStore64
600 pubArgument3
601 publicationRecordLengthAt
602 pubResult
603 (publicationValidateOccupiedSequences
604 ordinaryCapacity
605 (pubMove
606 pubArgument4
607 pubArgument1
608 (pubMove
609 pubScratch1
610 pubArgument3
611 (pubAddImmediate
612 pubScratch1
613 (naturalAdd publicationBodyAt publicationPayloadRecordsAt)
614 (pubLoad64
615 pubScratch0
616 pubArgument0
617 captureOrdinaryUsedAt
618 (pubMultiplyImmediate
619 pubScratch0
620 (naturalDivideUnchecked captureRecordBytes captureWordBytes)
621 (pubCompareImmediate
622 pubScratch0
623 0
624 (pubJumpIf
625 (constructor
626 TelemetryPublicationCondition
627 TelemetryPublicationZero)
628 b"publication-reserved-copy"
629 (pubLabel
630 b"publication-ordinary-copy"
631 (pubLoad64
632 pubResult
633 pubArgument1
634 0
635 (pubStore64
636 pubScratch1
637 0
638 pubResult
639 (pubAddImmediate
640 pubArgument1
641 captureWordBytes
642 (pubAddImmediate
643 pubScratch1
644 captureWordBytes
645 (pubAddImmediate
646 pubScratch0
647 0xffffffff
648 (pubJumpIf
649 (constructor
650 TelemetryPublicationCondition
651 TelemetryPublicationNotZero)
652 b"publication-ordinary-copy"
653 (pubLabel
654 b"publication-reserved-copy"
655 (publicationPrepareOccupiedRecords
656 ordinaryCapacity
657 reservedCapacity)))))))))))))))))))))))))))))))))))))))
658 in
659 (let unrestricted publicationPrepareSnapshot =
660 (lambda unrestricted ordinaryCapacity : Nat .
661 (lambda unrestricted reservedCapacity : Nat .
662 (pubOr
663 pubResult
664 pubScratch0
665 (pubCompareImmediate
666 pubResult
667 0
668 (pubJumpIf
669 (constructor
670 TelemetryPublicationCondition
671 TelemetryPublicationZero)
672 b"publication-prepare-reject"
673 (pubLoad64
674 pubResult
675 pubArgument3
676 publicationTerminalRequestAt
677 (pubStore8
678 pubArgument3
679 (naturalAdd
680 publicationBodyAt
681 (naturalSaturatingSubtract nativeTelemetryFlagsBytes 1))
682 pubResult
683 (pubLoad64
684 pubResult
685 pubArgument3
686 publicationBatchOrdinalAt
687 (pubStore64
688 pubArgument3
689 (naturalAdd publicationBodyAt nativeTelemetrySequenceAt)
690 pubResult
691 (pubLoad64
692 pubResult
693 pubArgument3
694 publicationPublishedNextAt
695 (pubStore64
696 pubArgument3
697 (naturalAdd
698 publicationBodyAt
699 nativeTelemetryEmptyErrorPayloadAt)
700 pubResult
701 (pubLoad64
702 pubResult
703 pubArgument0
704 (naturalMultiply 0 captureWordBytes)
705 (pubStore64
706 pubArgument3
707 (naturalAdd
708 publicationBodyAt
709 (naturalAdd
710 nativeTelemetryCountersAt
711 (naturalMultiply 0 captureWordBytes)))
712 pubResult
713 (pubLoad64
714 pubResult
715 pubArgument2
716 (naturalMultiply 0 captureWordBytes)
717 (pubStore64
718 pubArgument3
719 (naturalAdd
720 publicationBodyAt
721 (naturalAdd
722 nativeTelemetryIdentityAt
723 (naturalMultiply 0 captureWordBytes)))
724 pubResult
725 (pubLoad64
726 pubResult
727 pubArgument0
728 (naturalMultiply 1 captureWordBytes)
729 (pubStore64
730 pubArgument3
731 (naturalAdd
732 publicationBodyAt
733 (naturalAdd
734 nativeTelemetryCountersAt
735 (naturalMultiply 1 captureWordBytes)))
736 pubResult
737 (pubLoad64
738 pubResult
739 pubArgument2
740 (naturalMultiply 1 captureWordBytes)
741 (pubStore64
742 pubArgument3
743 (naturalAdd
744 publicationBodyAt
745 (naturalAdd
746 nativeTelemetryIdentityAt
747 (naturalMultiply 1 captureWordBytes)))
748 pubResult
749 (pubLoad64
750 pubResult
751 pubArgument0
752 (naturalMultiply 2 captureWordBytes)
753 (pubStore64
754 pubArgument3
755 (naturalAdd
756 publicationBodyAt
757 (naturalAdd
758 nativeTelemetryCountersAt
759 (naturalMultiply 2 captureWordBytes)))
760 pubResult
761 (pubLoad64
762 pubResult
763 pubArgument2
764 (naturalMultiply 2 captureWordBytes)
765 (pubStore64
766 pubArgument3
767 (naturalAdd
768 publicationBodyAt
769 (naturalAdd
770 nativeTelemetryIdentityAt
771 (naturalMultiply 2 captureWordBytes)))
772 pubResult
773 (pubLoad64
774 pubResult
775 pubArgument0
776 (naturalMultiply 3 captureWordBytes)
777 (pubStore64
778 pubArgument3
779 (naturalAdd
780 publicationBodyAt
781 (naturalAdd
782 nativeTelemetryCountersAt
783 (naturalMultiply 3 captureWordBytes)))
784 pubResult
785 (pubLoad64
786 pubResult
787 pubArgument2
788 (naturalMultiply 3 captureWordBytes)
789 (pubStore64
790 pubArgument3
791 (naturalAdd
792 publicationBodyAt
793 (naturalAdd
794 nativeTelemetryIdentityAt
795 (naturalMultiply 3 captureWordBytes)))
796 pubResult
797 (pubLoad64
798 pubResult
799 pubArgument0
800 (naturalMultiply 4 captureWordBytes)
801 (pubStore64
802 pubArgument3
803 (naturalAdd
804 publicationBodyAt
805 (naturalAdd
806 nativeTelemetryCountersAt
807 (naturalMultiply 4 captureWordBytes)))
808 pubResult
809 (pubLoad64
810 pubResult
811 pubArgument2
812 (naturalMultiply 4 captureWordBytes)
813 (pubStore64
814 pubArgument3
815 (naturalAdd
816 publicationBodyAt
817 (naturalAdd
818 nativeTelemetryIdentityAt
819 (naturalMultiply 4 captureWordBytes)))
820 pubResult
821 (pubLoad64
822 pubResult
823 pubArgument0
824 (naturalMultiply 5 captureWordBytes)
825 (pubStore64
826 pubArgument3
827 (naturalAdd
828 publicationBodyAt
829 (naturalAdd
830 nativeTelemetryCountersAt
831 (naturalMultiply 5 captureWordBytes)))
832 pubResult
833 (pubLoad64
834 pubResult
835 pubArgument2
836 (naturalMultiply 5 captureWordBytes)
837 (pubStore64
838 pubArgument3
839 (naturalAdd
840 publicationBodyAt
841 (naturalAdd
842 nativeTelemetryIdentityAt
843 (naturalMultiply 5 captureWordBytes)))
844 pubResult
845 (pubLoad64
846 pubResult
847 pubArgument0
848 (naturalMultiply 6 captureWordBytes)
849 (pubStore64
850 pubArgument3
851 (naturalAdd
852 publicationBodyAt
853 (naturalAdd
854 nativeTelemetryCountersAt
855 (naturalMultiply 6 captureWordBytes)))
856 pubResult
857 (publicationPrepareExtent ordinaryCapacity reservedCapacity))))))))))))))))))))))))))))))))))))))
858 in
859 (let unrestricted publicationPrepareIdentities =
860 (lambda unrestricted ordinaryCapacity : Nat .
861 (lambda unrestricted reservedCapacity : Nat .
862 (pubSubtract
863 pubResult
864 pubScratch0
865 (pubLoad64
866 pubScratch0
867 pubArgument0
868 captureDroppedAt
869 (pubLoad64
870 pubScratch1
871 pubArgument3
872 publicationPublishedDroppedAt
873 (pubCompare
874 pubScratch0
875 pubScratch1
876 (pubJumpIf
877 (constructor
878 TelemetryPublicationCondition
879 TelemetryPublicationBelow)
880 b"publication-prepare-reject"
881 (pubSubtract
882 pubScratch0
883 pubScratch1
884 (pubCompare
885 pubResult
886 pubScratch0
887 (pubJumpIf
888 (constructor
889 TelemetryPublicationCondition
890 TelemetryPublicationBelow)
891 b"publication-prepare-reject"
892 (pubSubtract
893 pubResult
894 pubScratch0
895 (pubLoad64
896 pubScratch0
897 pubArgument0
898 captureOrdinaryUsedAt
899 (pubLoad64
900 pubScratch1
901 pubArgument0
902 captureReservedUsedAt
903 (pubAdd
904 pubScratch0
905 pubScratch1
906 (pubCompare
907 pubResult
908 pubScratch0
909 (pubJumpIf
910 (constructor
911 TelemetryPublicationCondition
912 TelemetryPublicationNotZero)
913 b"publication-prepare-reject"
914 (pubLoad64
915 pubResult
916 pubArgument0
917 captureExcludedAt
918 (pubLoad64
919 pubScratch0
920 pubArgument3
921 publicationPublishedExcludedAt
922 (pubCompare
923 pubResult
924 pubScratch0
925 (pubJumpIf
926 (constructor
927 TelemetryPublicationCondition
928 TelemetryPublicationBelow)
929 b"publication-prepare-reject"
930 (pubLoad64
931 pubResult
932 pubArgument2
933 (telemetryIdentityOffset telemetryRunIdentityIndex)
934 (pubLoad64
935 pubScratch0
936 pubArgument2
937 (naturalAdd
938 (telemetryIdentityOffset telemetryRunIdentityIndex)
939 captureWordBytes)
940 (pubOr
941 pubResult
942 pubScratch0
943 (pubCompareImmediate
944 pubResult
945 0
946 (pubJumpIf
947 (constructor
948 TelemetryPublicationCondition
949 TelemetryPublicationZero)
950 b"publication-prepare-reject"
951 (pubLoad64
952 pubResult
953 pubArgument2
954 (telemetryIdentityOffset telemetryAttemptIdentityIndex)
955 (pubLoad64
956 pubScratch0
957 pubArgument2
958 (naturalAdd
959 (telemetryIdentityOffset telemetryAttemptIdentityIndex)
960 captureWordBytes)
961 (pubOr
962 pubResult
963 pubScratch0
964 (pubCompareImmediate
965 pubResult
966 0
967 (pubJumpIf
968 (constructor
969 TelemetryPublicationCondition
970 TelemetryPublicationZero)
971 b"publication-prepare-reject"
972 (pubLoad64
973 pubResult
974 pubArgument2
975 (telemetryIdentityOffset telemetryProducerIdentityIndex)
976 (pubLoad64
977 pubScratch0
978 pubArgument2
979 (naturalAdd
980 (telemetryIdentityOffset telemetryProducerIdentityIndex)
981 captureWordBytes)
982 (pubOr
983 pubResult
984 pubScratch0
985 (pubCompareImmediate
986 pubResult
987 0
988 (pubJumpIf
989 (constructor
990 TelemetryPublicationCondition
991 TelemetryPublicationZero)
992 b"publication-prepare-reject"
993 (pubLoad64
994 pubResult
995 pubArgument2
996 (telemetryIdentityOffset telemetryProducerEpochIndex)
997 (pubLoad64
998 pubScratch0
999 pubArgument2
1000 (naturalAdd
1001 (telemetryIdentityOffset telemetryProducerEpochIndex)
1002 captureWordBytes)
1003 (publicationPrepareSnapshot
1004 ordinaryCapacity
1005 reservedCapacity))))))))))))))))))))))))))))))))))))))
1006 in
1007 (let unrestricted publicationPrepareBoundsForBody =
1008 (lambda unrestricted ordinaryCapacity : Nat .
1009 (lambda unrestricted reservedCapacity : Nat .
1010 (lambda unrestricted bodyBytes : Nat .
1011 (pubCompareImmediate
1012 pubArgument4
1013 (captureQueueBytes ordinaryCapacity reservedCapacity)
1014 (pubJumpIf
1015 (constructor
1016 TelemetryPublicationCondition
1017 TelemetryPublicationNotZero)
1018 b"publication-prepare-reject"
1019 (pubCompareImmediate
1020 pubArgument5
1021 (publicationArenaBytesForBody bodyBytes)
1022 (pubJumpIf
1023 (constructor
1024 TelemetryPublicationCondition
1025 TelemetryPublicationNotZero)
1026 b"publication-prepare-reject"
1027 (pubLoad64
1028 pubResult
1029 pubArgument0
1030 captureOrdinaryCapacityAt
1031 (pubCompareImmediate
1032 pubResult
1033 ordinaryCapacity
1034 (pubJumpIf
1035 (constructor
1036 TelemetryPublicationCondition
1037 TelemetryPublicationNotZero)
1038 b"publication-prepare-reject"
1039 (pubLoad64
1040 pubResult
1041 pubArgument0
1042 captureReservedCapacityAt
1043 (pubCompareImmediate
1044 pubResult
1045 reservedCapacity
1046 (pubJumpIf
1047 (constructor
1048 TelemetryPublicationCondition
1049 TelemetryPublicationNotZero)
1050 b"publication-prepare-reject"
1051 (pubLoad64
1052 pubResult
1053 pubArgument0
1054 captureRequiredAt
1055 (pubCompareImmediate
1056 pubResult
1057 1
1058 (pubJumpIf
1059 (constructor
1060 TelemetryPublicationCondition
1061 TelemetryPublicationAbove)
1062 b"publication-prepare-reject"
1063 (pubLoad64
1064 pubResult
1065 pubArgument0
1066 captureOrdinaryUsedAt
1067 (pubCompareImmediate
1068 pubResult
1069 ordinaryCapacity
1070 (pubJumpIf
1071 (constructor
1072 TelemetryPublicationCondition
1073 TelemetryPublicationAbove)
1074 b"publication-prepare-reject"
1075 (pubLoad64
1076 pubResult
1077 pubArgument0
1078 captureReservedUsedAt
1079 (pubCompareImmediate
1080 pubResult
1081 reservedCapacity
1082 (pubJumpIf
1083 (constructor
1084 TelemetryPublicationCondition
1085 TelemetryPublicationAbove)
1086 b"publication-prepare-reject"
1087 (pubLoad64
1088 pubResult
1089 pubArgument3
1090 publicationFinishedAt
1091 (pubCompareImmediate
1092 pubResult
1093 0
1094 (pubJumpIf
1095 (constructor
1096 TelemetryPublicationCondition
1097 TelemetryPublicationNotZero)
1098 b"publication-prepare-reject"
1099 (pubLoad64
1100 pubResult
1101 pubArgument3
1102 publicationPoisonedAt
1103 (pubCompareImmediate
1104 pubResult
1105 0
1106 (pubJumpIf
1107 (constructor
1108 TelemetryPublicationCondition
1109 TelemetryPublicationNotZero)
1110 b"publication-prepare-reject"
1111 (pubLoad64
1112 pubResult
1113 pubArgument3
1114 publicationTerminalRequestAt
1115 (pubCompareImmediate
1116 pubResult
1117 1
1118 (pubJumpIf
1119 (constructor
1120 TelemetryPublicationCondition
1121 TelemetryPublicationAbove)
1122 b"publication-prepare-reject"
1123 (pubLoad64
1124 pubResult
1125 pubArgument3
1126 publicationBatchOrdinalAt
1127 (pubCompareImmediate
1128 pubResult
1129 0xffffffff
1130 (pubJumpIf
1131 (constructor
1132 TelemetryPublicationCondition
1133 TelemetryPublicationZero)
1134 b"publication-prepare-reject"
1135 (pubLoad64
1136 pubResult
1137 pubArgument0
1138 captureNextSequenceAt
1139 (pubLoad64
1140 pubScratch0
1141 pubArgument3
1142 publicationPublishedNextAt
1143 (pubCompare
1144 pubResult
1145 pubScratch0
1146 (pubJumpIf
1147 (constructor
1148 TelemetryPublicationCondition
1149 TelemetryPublicationBelow)
1150 b"publication-prepare-reject"
1151 (publicationPrepareIdentities
1152 ordinaryCapacity
1153 reservedCapacity)))))))))))))))))))))))))))))))))))))))
1154 in
1155 (let unrestricted publicationTypedPayloadLengths =
1156 (pubMove
1157 pubArgument3
1158 pubArgument0
1159 (pubStore64
1160 pubArgument3
1161 (naturalAdd
1162 publicationBodyAt
1163 nativeTelemetryEmptyErrorPayloadExtentAt)
1164 pubArgument2
1165 (pubMove
1166 pubResult
1167 pubArgument2
1168 (pubAddImmediate
1169 pubResult
1170 nativeTelemetryEmptyErrorPayloadAt
1171 (pubStore64
1172 pubArgument3
1173 publicationBodyLengthAt
1174 pubResult
1175 (pubMove
1176 pubScratch1
1177 pubArgument3
1178 (pubAddImmediate
1179 pubScratch1
1180 publicationBodyAt
1181 (pubAdd
1182 pubScratch1
1183 pubResult
1184 (pubMove
1185 pubScratch0
1186 pubResult
1187 (pubAddImmediate
1188 pubScratch0
1189 (naturalAdd 1 (naturalAdd nativeTelemetryScalarBytes 63))
1190 (pubShiftRight
1191 pubScratch0
1192 6
1193 (pubStore64
1194 pubArgument3
1195 publicationBlockCountAt
1196 pubScratch0
1197 (pubAddImmediate
1198 pubResult
1199 (naturalAdd
1200 (bytes-length nativeTelemetryMagic)
1201 nativeTelemetryDigestBytes)
1202 (pubStore64
1203 pubArgument3
1204 publicationRecordLengthAt
1205 pubResult
1206 (pubSet
1207 pubResult
1208 3
1209 (pubStore8
1210 pubArgument3
1211 publicationBodyAt
1212 pubResult
1213 publicationPadPreparedBody))))))))))))))))
1214 in
1215 (let unrestricted publicationTypedPayloadBounds =
1216 (lambda unrestricted bodyBytes : Nat .
1217 (pubCompareImmediate
1218 pubArgument1
1219 (publicationArenaBytesForBody bodyBytes)
1220 (pubJumpIf
1221 (constructor
1222 TelemetryPublicationCondition
1223 TelemetryPublicationNotZero)
1224 b"publication-prepare-reject"
1225 (pubLoad64
1226 pubResult
1227 pubArgument0
1228 publicationReadyAt
1229 (pubSet
1230 pubScratch0
1231 0
1232 (pubStore64
1233 pubArgument0
1234 publicationReadyAt
1235 pubScratch0
1236 (pubCompareImmediate
1237 pubResult
1238 1
1239 (pubJumpIf
1240 (constructor
1241 TelemetryPublicationCondition
1242 TelemetryPublicationNotZero)
1243 b"publication-prepare-reject"
1244 (pubSet
1245 pubResult
1246 0
1247 (pubStore64
1248 pubArgument0
1249 publicationReadyAt
1250 pubResult
1251 (pubLoad64
1252 pubResult
1253 pubArgument0
1254 publicationPoisonedAt
1255 (pubCompareImmediate
1256 pubResult
1257 0
1258 (pubJumpIf
1259 (constructor
1260 TelemetryPublicationCondition
1261 TelemetryPublicationNotZero)
1262 b"publication-prepare-reject"
1263 (pubLoad64
1264 pubResult
1265 pubArgument0
1266 publicationFinishedAt
1267 (pubCompareImmediate
1268 pubResult
1269 0
1270 (pubJumpIf
1271 (constructor
1272 TelemetryPublicationCondition
1273 TelemetryPublicationNotZero)
1274 b"publication-prepare-reject"
1275 (pubCompareImmediate
1276 pubArgument2
1277 captureWordBytes
1278 (pubJumpIf
1279 (constructor
1280 TelemetryPublicationCondition
1281 TelemetryPublicationBelow)
1282 b"publication-prepare-reject"
1283 (pubCompareImmediate
1284 pubArgument2
1285 (naturalSaturatingSubtract
1286 bodyBytes
1287 nativeTelemetryEmptyErrorPayloadAt)
1288 (pubJumpIf
1289 (constructor
1290 TelemetryPublicationCondition
1291 TelemetryPublicationAbove)
1292 b"publication-prepare-reject"
1293 publicationTypedPayloadLengths))))))))))))))))))))
1294 in
1295 (let unrestricted publicationCommitRestore =
1296 (pubSet
1297 pubResult
1298 5
1299 (pubJump
1300 b"publication-cleanup"
1301 (pubLabel
1302 b"publication-invalid"
1303 (pubSet
1304 pubResult
1305 4
1306 (pubJump
1307 b"publication-cleanup"
1308 (pubLabel
1309 b"publication-cleanup"
1310 (pubLoad64
1311 pubPersistent0
1312 pubPersistent1
1313 publicationSavedR12At
1314 (pubLoad64
1315 pubPersistent2
1316 pubPersistent1
1317 publicationSavedR14At
1318 (pubLoad64
1319 pubPersistent3
1320 pubPersistent1
1321 publicationSavedR15At
1322 (pubLoad64
1323 pubPersistent1
1324 pubPersistent1
1325 publicationSavedR13At
1326 (pubReturn pubEnd)))))))))))
1327 in
1328 (let unrestricted publicationCommitSyncAndReclaim =
1329 (pubJumpIf
1330 (constructor
1331 TelemetryPublicationCondition
1332 TelemetryPublicationNotZero)
1333 b"publication-sync-failure"
1334 (pubLoad64
1335 pubResult
1336 pubPersistent0
1337 captureNextSequenceAt
1338 (pubStore64
1339 pubPersistent1
1340 publicationPublishedNextAt
1341 pubResult
1342 (pubLoad64
1343 pubResult
1344 pubPersistent0
1345 captureDroppedAt
1346 (pubStore64
1347 pubPersistent1
1348 publicationPublishedDroppedAt
1349 pubResult
1350 (pubLoad64
1351 pubResult
1352 pubPersistent0
1353 captureExcludedAt
1354 (pubStore64
1355 pubPersistent1
1356 publicationPublishedExcludedAt
1357 pubResult
1358 (pubLoad64
1359 pubResult
1360 pubPersistent1
1361 publicationTerminalRequestAt
1362 (pubStore64
1363 pubPersistent1
1364 publicationFinishedAt
1365 pubResult
1366 (pubLoad64
1367 pubResult
1368 pubPersistent1
1369 publicationBatchOrdinalAt
1370 (pubAddImmediate
1371 pubResult
1372 1
1373 (pubStore64
1374 pubPersistent1
1375 publicationBatchOrdinalAt
1376 pubResult
1377 (pubSet
1378 pubResult
1379 0
1380 (pubStore64
1381 pubPersistent0
1382 captureOrdinaryUsedAt
1383 pubResult
1384 (pubStore64
1385 pubPersistent0
1386 captureReservedUsedAt
1387 pubResult
1388 (pubJump
1389 b"publication-cleanup"
1390 (pubLabel
1391 b"publication-write-failure"
1392 (pubSet
1393 pubResult
1394 1
1395 (pubStore64
1396 pubPersistent1
1397 publicationPoisonedAt
1398 pubResult
1399 (pubSet
1400 pubResult
1401 2
1402 (pubJump
1403 b"publication-cleanup"
1404 (pubLabel
1405 b"publication-sync-failure"
1406 (pubSet
1407 pubResult
1408 1
1409 (pubStore64
1410 pubPersistent1
1411 publicationPoisonedAt
1412 pubResult
1413 (pubSet
1414 pubResult
1415 3
1416 (pubJump
1417 b"publication-cleanup"
1418 (pubLabel
1419 b"publication-poisoned"
1420 (pubSet
1421 pubResult
1422 6
1423 (pubJump
1424 b"publication-cleanup"
1425 (pubLabel b"publication-closed" publicationCommitRestore))))))))))))))))))))))))))))))
1426 in
1427 (let unrestricted publicationCommitWrite =
1428 (pubStore64
1429 pubArgument1
1430 publicationSavedR12At
1431 pubPersistent0
1432 (pubStore64
1433 pubArgument1
1434 publicationSavedR13At
1435 pubPersistent1
1436 (pubStore64
1437 pubArgument1
1438 publicationSavedR14At
1439 pubPersistent2
1440 (pubStore64
1441 pubArgument1
1442 publicationSavedR15At
1443 pubPersistent3
1444 (pubMove
1445 pubPersistent0
1446 pubArgument0
1447 (pubMove
1448 pubPersistent1
1449 pubArgument1
1450 (pubMove
1451 pubPersistent2
1452 pubArgument2
1453 (pubMove
1454 pubPersistent3
1455 pubArgument5
1456 (pubLoad64
1457 pubResult
1458 pubPersistent1
1459 publicationRecordLengthAt
1460 (pubCompare
1461 pubArgument4
1462 pubResult
1463 (pubJumpIf
1464 (constructor
1465 TelemetryPublicationCondition
1466 TelemetryPublicationNotZero)
1467 b"publication-invalid"
1468 (pubCompareImmediate
1469 pubArgument4
1470 (publicationRecordBytes publicationPayloadRecordsAt)
1471 (pubJumpIf
1472 (constructor
1473 TelemetryPublicationCondition
1474 TelemetryPublicationBelow)
1475 b"publication-invalid"
1476 (pubCompareImmediate
1477 pubArgument4
1478 publicationMaximumFrameBytes
1479 (pubJumpIf
1480 (constructor
1481 TelemetryPublicationCondition
1482 TelemetryPublicationAbove)
1483 b"publication-invalid"
1484 (pubLoad64
1485 pubResult
1486 pubPersistent1
1487 publicationBatchOrdinalAt
1488 (pubCompareImmediate
1489 pubResult
1490 0xffffffff
1491 (pubJumpIf
1492 (constructor
1493 TelemetryPublicationCondition
1494 TelemetryPublicationZero)
1495 b"publication-invalid"
1496 (pubLoad64
1497 pubResult
1498 pubPersistent1
1499 publicationTerminalRequestAt
1500 (pubCompareImmediate
1501 pubResult
1502 1
1503 (pubJumpIf
1504 (constructor
1505 TelemetryPublicationCondition
1506 TelemetryPublicationAbove)
1507 b"publication-invalid"
1508 (pubSet
1509 pubResult
1510 0
1511 (pubStore64
1512 pubPersistent1
1513 publicationReadyAt
1514 pubResult
1515 (pubLoad64
1516 pubResult
1517 pubPersistent1
1518 publicationPoisonedAt
1519 (pubCompareImmediate
1520 pubResult
1521 0
1522 (pubJumpIf
1523 (constructor
1524 TelemetryPublicationCondition
1525 TelemetryPublicationNotZero)
1526 b"publication-poisoned"
1527 (pubLoad64
1528 pubResult
1529 pubPersistent1
1530 publicationFinishedAt
1531 (pubCompareImmediate
1532 pubResult
1533 0
1534 (pubJumpIf
1535 (constructor
1536 TelemetryPublicationCondition
1537 TelemetryPublicationNotZero)
1538 b"publication-closed"
1539 (pubMove
1540 pubArgument0
1541 pubPersistent2
1542 (pubMove
1543 pubArgument1
1544 pubArgument3
1545 (pubMove
1546 pubArgument2
1547 pubArgument4
1548 (pubWrite
1549 (pubCompare
1550 pubResult
1551 pubArgument4
1552 (pubJumpIf
1553 (constructor
1554 TelemetryPublicationCondition
1555 TelemetryPublicationNotZero)
1556 b"publication-write-failure"
1557 (pubMove
1558 pubArgument0
1559 pubPersistent2
1560 (pubSync
1561 (pubCompareImmediate
1562 pubResult
1563 0
1564 (pubJumpIf
1565 (constructor
1566 TelemetryPublicationCondition
1567 TelemetryPublicationNotZero)
1568 b"publication-sync-failure"
1569 (pubMove
1570 pubArgument0
1571 pubPersistent3
1572 (pubSync
1573 (pubCompareImmediate
1574 pubResult
1575 0
1576 publicationCommitSyncAndReclaim))))))))))))))))))))))))))))))))))))))))))
1577 in
1578 (eliminate
1579 TelemetryPublicationRoutineKind
1580 (lambda unrestricted current : (family TelemetryPublicationRoutineKind) .
1581 A)
1582 kind
1583 (branch
1584 TelemetryPublicationPrepareRoutine
1585 ordinary
1586 reserved
1587 bound
1588 .
1589 (publicationPrepareBoundsForBody ordinary reserved bound))
1590 (branch
1591 TelemetryPublicationTypedPaddingRoutine
1592 bound
1593 .
1594 (publicationTypedPayloadBounds bound))
1595 (branch
1596 TelemetryPublicationCommitRoutine
1597 .
1598 publicationCommitWrite))))))))))))))))))))))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.