1module Runtime.TelemetryPolicyRoutine
2
3import Observe.Value
4import Runtime.TelemetryCapture
5import Runtime.TelemetryPublication
6import Std.Natural
7
8-- Shared leaf algorithms for selection, unsigned source arithmetic, flush
9-- cadence and continuation. Emitters own the calling convention and preserve
10-- their host interpreter's persistent registers. Word operations wrap at 64
11-- bits; loads/stores are little-endian. Add supplies Below iff unsigned carry
12-- occurred. Compare supplies unsigned order. Divide takes Result with zero
13-- Argument2 as the unsigned dividend, returns quotient in Result and remainder
14-- in Argument2, and requires a positive divisor. Multiply supplies the wrapped
15-- low product in Result and may clobber Argument2; no high-product claim.
16-- SetWord retains all 64 bits, unlike an ISA's smaller immediate fields.
17family TelemetryPolicyCondition : Type 0
18constructor TelemetryPolicyZero
19constructor TelemetryPolicyNotZero
20constructor TelemetryPolicyBelow
21constructor TelemetryPolicyAbove
22
23end-family
24
25family TelemetryPolicyBackend : Type 0
26parameter erased A : Type 0
27parameter erased R : Type 0
28constructor TelemetryPolicyBackendValue
29field unrestricted backendPolicySet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
30field unrestricted backendPolicySetWord : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
31field unrestricted backendPolicyMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
32field unrestricted backendPolicyStore : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A))))
33field unrestricted backendPolicyLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A))))
34field unrestricted backendPolicyCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
35field unrestricted backendPolicyCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
36field unrestricted backendPolicySubtract : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
37field unrestricted backendPolicyAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
38field unrestricted backendPolicyDivide : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A))
39field unrestricted backendPolicyMultiply : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A))
40field unrestricted backendPolicyJumpIf : (pi unrestricted a0 : (family TelemetryPolicyCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A)))
41field unrestricted backendPolicyJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
42field unrestricted backendPolicyLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
43field unrestricted backendPolicyReturn : (pi unrestricted a0 : A . A)
44field unrestricted backendPolicyEnd : A
45field unrestricted backendPolicyResult : R
46field unrestricted backendPolicyArgument0 : R
47field unrestricted backendPolicyArgument1 : R
48field unrestricted backendPolicyArgument2 : R
49field unrestricted backendPolicyArgument3 : R
50field unrestricted backendPolicyArgument4 : R
51field unrestricted backendPolicyArgument5 : R
52field unrestricted backendPolicyScratch0 : R
53field unrestricted backendPolicyScratch1 : R
54
55end-family
56
57def telemetryPolicySiteAssemblyFor =
58 (lambda erased A : Type 0 .
59 (lambda erased R : Type 0 .
60 (lambda unrestricted backend : (family TelemetryPolicyBackend A R) .
61 (lambda unrestricted ordinaryCapacity : Nat .
62 (lambda unrestricted reservedCapacity : Nat .
63 (lambda unrestricted required : Nat .
64 (lambda unrestricted enabled : Nat .
65 (lambda unrestricted stride : Nat .
66 (lambda unrestricted bound : Nat .
67 (eliminate
68 TelemetryPolicyBackend
69 (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A)
70 backend
71 (branch
72 TelemetryPolicyBackendValue
73 policySet
74 policySetWord
75 policyMove
76 policyStore
77 policyLoad
78 policyCompareImmediate
79 policyCompare
80 policySubtract
81 policyAdd
82 policyDivide
83 policyMultiply
84 policyJumpIf
85 policyJump
86 policyLabel
87 policyReturn
88 policyEnd
89 policyResult
90 policyArgument0
91 policyArgument1
92 policyArgument2
93 policyArgument3
94 policyArgument4
95 policyArgument5
96 policyScratch0
97 policyScratch1
98 .
99 (policySet
100 policyResult
101 4
102 (policyStore
103 policyArgument3
104 0
105 policyResult
106 (policyCompareImmediate
107 policyArgument4
108 (publicationArenaBytesForBody bound)
109 (policyJumpIf
110 (constructor TelemetryPolicyCondition TelemetryPolicyNotZero)
111 b"site-refused"
112 (policyLoad
113 policyResult
114 policyArgument0
115 captureOrdinaryCapacityAt
116 (policyCompareImmediate
117 policyResult
118 ordinaryCapacity
119 (policyJumpIf
120 (constructor TelemetryPolicyCondition TelemetryPolicyNotZero)
121 b"site-refused"
122 (policyLoad
123 policyResult
124 policyArgument0
125 captureReservedCapacityAt
126 (policyCompareImmediate
127 policyResult
128 reservedCapacity
129 (policyJumpIf
130 (constructor
131 TelemetryPolicyCondition
132 TelemetryPolicyNotZero)
133 b"site-refused"
134 (policyLoad
135 policyResult
136 policyArgument0
137 captureRequiredAt
138 (policyCompareImmediate
139 policyResult
140 required
141 (policyJumpIf
142 (constructor
143 TelemetryPolicyCondition
144 TelemetryPolicyNotZero)
145 b"site-refused"
146 (policyLoad
147 policyResult
148 policyArgument1
149 publicationFinishedAt
150 (policyCompareImmediate
151 policyResult
152 0
153 (policyJumpIf
154 (constructor
155 TelemetryPolicyCondition
156 TelemetryPolicyNotZero)
157 b"site-refused"
158 (aosChoose
159 A
160 enabled
161 (aosChoose
162 A
163 (naturalEqual stride 1)
164 (policySet
165 policyResult
166 1
167 (policyStore
168 policyArgument3
169 0
170 policyResult
171 (policySet
172 policyResult
173 1
174 (policyReturn
175 (policyLabel
176 b"site-excluded"
177 (policySet
178 policyResult
179 0
180 (policyStore
181 policyArgument3
182 0
183 policyResult
184 (policySet
185 policyResult
186 1
187 (policyReturn
188 (policyLabel
189 b"site-refused"
190 (policySet policyResult 0 (policyReturn policyEnd))))))))))))
191 (policyMove
192 policyResult
193 policyArgument2
194 (policySet
195 policyArgument2
196 0
197 (policySetWord
198 policyArgument4
199 stride
200 (policyDivide
201 policyArgument4
202 (policyCompareImmediate
203 policyArgument2
204 0
205 (policyJumpIf
206 (constructor
207 TelemetryPolicyCondition
208 TelemetryPolicyNotZero)
209 b"site-excluded"
210 (policySet
211 policyResult
212 1
213 (policyStore
214 policyArgument3
215 0
216 policyResult
217 (policySet
218 policyResult
219 1
220 (policyReturn
221 (policyLabel
222 b"site-excluded"
223 (policySet
224 policyResult
225 0
226 (policyStore
227 policyArgument3
228 0
229 policyResult
230 (policySet
231 policyResult
232 1
233 (policyReturn
234 (policyLabel
235 b"site-refused"
236 (policySet policyResult 0 (policyReturn policyEnd)))))))))))))))))))
237 (policyJump
238 b"site-excluded"
239 (policySet
240 policyResult
241 1
242 (policyStore
243 policyArgument3
244 0
245 policyResult
246 (policySet
247 policyResult
248 1
249 (policyReturn
250 (policyLabel
251 b"site-excluded"
252 (policySet
253 policyResult
254 0
255 (policyStore
256 policyArgument3
257 0
258 policyResult
259 (policySet
260 policyResult
261 1
262 (policyReturn
263 (policyLabel
264 b"site-refused"
265 (policySet policyResult 0 (policyReturn policyEnd)))))))))))))))))))))))))))))))))))))))))
266
267def telemetryPolicyFlushAssemblyFor =
268 (lambda erased A : Type 0 .
269 (lambda erased R : Type 0 .
270 (lambda unrestricted backend : (family TelemetryPolicyBackend A R) .
271 (lambda unrestricted threshold : Nat .
272 (lambda unrestricted bound : Nat .
273 (eliminate
274 TelemetryPolicyBackend
275 (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A)
276 backend
277 (branch
278 TelemetryPolicyBackendValue
279 policySet
280 policySetWord
281 policyMove
282 policyStore
283 policyLoad
284 policyCompareImmediate
285 policyCompare
286 policySubtract
287 policyAdd
288 policyDivide
289 policyMultiply
290 policyJumpIf
291 policyJump
292 policyLabel
293 policyReturn
294 policyEnd
295 policyResult
296 policyArgument0
297 policyArgument1
298 policyArgument2
299 policyArgument3
300 policyArgument4
301 policyArgument5
302 policyScratch0
303 policyScratch1
304 .
305 (policySet
306 policyResult
307 7
308 (policyStore
309 policyArgument4
310 0
311 policyResult
312 (policyCompareImmediate
313 policyArgument5
314 (publicationArenaBytesForBody bound)
315 (policyJumpIf
316 (constructor TelemetryPolicyCondition TelemetryPolicyNotZero)
317 b"policy-flush-invalid"
318 (policyCompareImmediate
319 policyArgument3
320 1
321 (policyJumpIf
322 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
323 b"policy-flush-invalid"
324 (policyCompareImmediate
325 policyArgument2
326 4
327 (policyJumpIf
328 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
329 b"policy-flush-invalid"
330 (policyJumpIf
331 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
332 b"policy-flush-invalid"
333 (policyLoad
334 policyResult
335 policyArgument1
336 publicationFinishedAt
337 (policyCompareImmediate
338 policyResult
339 1
340 (policyJumpIf
341 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
342 b"policy-flush-invalid"
343 (policyJumpIf
344 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
345 b"policy-flush-closed"
346 (policyLoad
347 policyResult
348 policyArgument1
349 publicationPoisonedAt
350 (policyCompareImmediate
351 policyResult
352 1
353 (policyJumpIf
354 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
355 b"policy-flush-invalid"
356 (policyJumpIf
357 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
358 b"policy-flush-poisoned"
359 (policyCompareImmediate
360 policyArgument2
361 3
362 (policyJumpIf
363 (constructor
364 TelemetryPolicyCondition
365 TelemetryPolicyNotZero)
366 b"policy-flush-terminal"
367 (policyCompareImmediate
368 policyArgument3
369 1
370 (policyJumpIf
371 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
372 b"policy-flush-invalid"
373 (policyJump
374 b"policy-flush-requested"
375 (policyLabel
376 b"policy-flush-terminal"
377 (policyCompareImmediate
378 policyArgument3
379 1
380 (policyJumpIf
381 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
382 b"policy-flush-requested"
383 (policySetWord
384 policyArgument5
385 threshold
386 (policyLoad
387 policyResult
388 policyArgument0
389 captureNextSequenceAt
390 (policyLoad
391 policyScratch0
392 policyArgument1
393 publicationPublishedNextAt
394 (policyCompare
395 policyResult
396 policyScratch0
397 (policyJumpIf
398 (constructor TelemetryPolicyCondition TelemetryPolicyBelow)
399 b"policy-flush-invalid"
400 (policySubtract
401 policyResult
402 policyScratch0
403 (policyCompare
404 policyResult
405 policyArgument5
406 (policyJumpIf
407 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
408 b"policy-flush-requested"
409 (policyJumpIf
410 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
411 b"policy-flush-requested"
412 (policyLoad
413 policyScratch1
414 policyArgument0
415 captureExcludedAt
416 (policyLoad
417 policyScratch0
418 policyArgument1
419 publicationPublishedExcludedAt
420 (policyCompare
421 policyScratch1
422 policyScratch0
423 (policyJumpIf
424 (constructor TelemetryPolicyCondition TelemetryPolicyBelow)
425 b"policy-flush-invalid"
426 (policySubtract
427 policyScratch1
428 policyScratch0
429 (policyCompare
430 policyScratch1
431 policyArgument5
432 (policyJumpIf
433 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
434 b"policy-flush-requested"
435 (policyJumpIf
436 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
437 b"policy-flush-requested"
438 (policyAdd
439 policyResult
440 policyScratch1
441 (policyJumpIf
442 (constructor TelemetryPolicyCondition TelemetryPolicyBelow)
443 b"policy-flush-requested"
444 (policyCompare
445 policyResult
446 policyArgument5
447 (policyJumpIf
448 (constructor TelemetryPolicyCondition TelemetryPolicyAbove)
449 b"policy-flush-requested"
450 (policyJumpIf
451 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
452 b"policy-flush-requested"
453 (policySet
454 policyResult
455 0
456 (policyReturn
457 (policyLabel
458 b"policy-flush-requested"
459 (policySet
460 policyResult
461 1
462 (policyReturn
463 (policyLabel
464 b"policy-flush-invalid"
465 (policySet
466 policyResult
467 4
468 (policyStore
469 policyArgument4
470 0
471 policyResult
472 (policySet
473 policyResult
474 0
475 (policyReturn
476 (policyLabel
477 b"policy-flush-closed"
478 (policySet
479 policyResult
480 5
481 (policyStore
482 policyArgument4
483 0
484 policyResult
485 (policySet
486 policyResult
487 0
488 (policyReturn
489 (policyLabel
490 b"policy-flush-poisoned"
491 (policySet
492 policyResult
493 6
494 (policyStore
495 policyArgument4
496 0
497 policyResult
498 (policySet policyResult 0 (policyReturn policyEnd))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
499
500def telemetryPolicyAffineAssemblyFor =
501 (lambda erased A : Type 0 .
502 (lambda erased R : Type 0 .
503 (lambda unrestricted backend : (family TelemetryPolicyBackend A R) .
504 (eliminate
505 TelemetryPolicyBackend
506 (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A)
507 backend
508 (branch
509 TelemetryPolicyBackendValue
510 policySet
511 policySetWord
512 policyMove
513 policyStore
514 policyLoad
515 policyCompareImmediate
516 policyCompare
517 policySubtract
518 policyAdd
519 policyDivide
520 policyMultiply
521 policyJumpIf
522 policyJump
523 policyLabel
524 policyReturn
525 policyEnd
526 policyResult
527 policyArgument0
528 policyArgument1
529 policyArgument2
530 policyArgument3
531 policyArgument4
532 policyArgument5
533 policyScratch0
534 policyScratch1
535 .
536 (policyMove
537 policyResult
538 policyArgument0
539 (policyMove
540 policyArgument4
541 policyArgument2
542 (policyMultiply
543 policyArgument4
544 (policyAdd
545 policyResult
546 policyArgument1
547 (policyStore
548 policyArgument3
549 0
550 policyResult
551 (policySet policyResult 0 (policyReturn policyEnd))))))))))))
552
553def telemetryPolicyPendingAssemblyFor =
554 (lambda erased A : Type 0 .
555 (lambda erased R : Type 0 .
556 (lambda unrestricted backend : (family TelemetryPolicyBackend A R) .
557 (eliminate
558 TelemetryPolicyBackend
559 (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A)
560 backend
561 (branch
562 TelemetryPolicyBackendValue
563 policySet
564 policySetWord
565 policyMove
566 policyStore
567 policyLoad
568 policyCompareImmediate
569 policyCompare
570 policySubtract
571 policyAdd
572 policyDivide
573 policyMultiply
574 policyJumpIf
575 policyJump
576 policyLabel
577 policyReturn
578 policyEnd
579 policyResult
580 policyArgument0
581 policyArgument1
582 policyArgument2
583 policyArgument3
584 policyArgument4
585 policyArgument5
586 policyScratch0
587 policyScratch1
588 .
589 (policyCompareImmediate
590 policyArgument0
591 3
592 (policyJumpIf
593 (constructor TelemetryPolicyCondition TelemetryPolicyNotZero)
594 b"capture-not-pending"
595 (policySet
596 policyResult
597 1
598 (policyReturn
599 (policyLabel
600 b"capture-not-pending"
601 (policySet policyResult 0 (policyReturn policyEnd))))))))))))
602
603def telemetryPolicyContinuationAssemblyFor =
604 (lambda erased A : Type 0 .
605 (lambda erased R : Type 0 .
606 (lambda unrestricted backend : (family TelemetryPolicyBackend A R) .
607 (lambda unrestricted required : Nat .
608 (eliminate
609 TelemetryPolicyBackend
610 (lambda unrestricted current : (family TelemetryPolicyBackend A R) . A)
611 backend
612 (branch
613 TelemetryPolicyBackendValue
614 policySet
615 policySetWord
616 policyMove
617 policyStore
618 policyLoad
619 policyCompareImmediate
620 policyCompare
621 policySubtract
622 policyAdd
623 policyDivide
624 policyMultiply
625 policyJumpIf
626 policyJump
627 policyLabel
628 policyReturn
629 policyEnd
630 policyResult
631 policyArgument0
632 policyArgument1
633 policyArgument2
634 policyArgument3
635 policyArgument4
636 policyArgument5
637 policyScratch0
638 policyScratch1
639 .
640 (policyCompareImmediate
641 policyArgument0
642 1
643 (policyJumpIf
644 (constructor TelemetryPolicyCondition TelemetryPolicyBelow)
645 b"capture-continuation-allowed"
646 (policyJumpIf
647 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
648 b"capture-continuation-allowed"
649 (aosChoose
650 A
651 (naturalEqual required 0)
652 (policyCompareImmediate
653 policyArgument0
654 2
655 (policyJumpIf
656 (constructor TelemetryPolicyCondition TelemetryPolicyZero)
657 b"capture-continuation-allowed"
658 (policySet
659 policyResult
660 0
661 (policyReturn
662 (policyLabel
663 b"capture-continuation-allowed"
664 (policySet policyResult 1 (policyReturn policyEnd)))))))
665 (policySet
666 policyResult
667 0
668 (policyReturn
669 (policyLabel
670 b"capture-continuation-allowed"
671 (policySet policyResult 1 (policyReturn policyEnd)))))))))))))))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.