1module Runtime.TelemetryDrainRoutine
2
3import Observe.Value
4import Runtime.NativeTelemetry
5import Runtime.TelemetryCapture
6import Runtime.TelemetryDrain
7import Runtime.TelemetryPublication
8import Runtime.TelemetryRecord
9import Std.Natural
10
11-- Single-writer staging and private route metadata, shared across host ISAs.
12-- The caller supplies live disjoint certified arenas and serializes capture,
13-- drain and commit. Extent checks precede loads/stores where the ABI supplies
14-- an extent. A failed accessible append/read clears readiness; an inaccessible
15-- publication extent must not dereference its pointer. Success only grants
16-- private staging: none of these routines writes a file or acknowledges data.
17-- Word operations wrap at 64 bits, comparisons are unsigned, and Divide uses
18-- Result with zero Argument2 as its dividend and positive Scratch0 divisor.
19-- Set retains its admitted 32-bit immediate, AddImmediate sign-extends it.
20family TelemetryDrainCondition : Type 0
21constructor TelemetryDrainZero
22constructor TelemetryDrainNotZero
23constructor TelemetryDrainBelow
24constructor TelemetryDrainAbove
25
26end-family
27
28family TelemetryDrainRoutineKind : Type 0
29constructor TelemetryDrainReadyRoutine
30constructor TelemetryDrainAppendRoutine
31field unrestricted drainAppendBound : Nat
32constructor TelemetryDrainCommitTagRoutine
33field unrestricted drainCommitOrdinary : Nat
34field unrestricted drainCommitReserved : Nat
35field unrestricted drainCommitRole : Nat
36field unrestricted drainCommitTag : Nat
37constructor TelemetryDrainReadTagRoutine
38field unrestricted drainReadOrdinary : Nat
39field unrestricted drainReadReserved : Nat
40field unrestricted drainReadRoutes : (family TelemetryRecordRoutes)
41constructor TelemetryDrainMatchTagRoutine
42field unrestricted drainMatchTag : Nat
43
44end-family
45
46family TelemetryDrainBackend : Type 0
47parameter erased A : Type 0
48parameter erased R : Type 0
49constructor TelemetryDrainBackendValue
50field unrestricted backendDrainSet : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
51field unrestricted backendDrainMove : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
52field unrestricted backendDrainLoad : (pi unrestricted destination : R . (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted tail : A . A))))
53field unrestricted backendDrainStore64 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A))))
54field unrestricted backendDrainStore8 : (pi unrestricted base : R . (pi unrestricted offset : Nat . (pi unrestricted value : R . (pi unrestricted tail : A . A))))
55field unrestricted backendDrainCompareImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
56field unrestricted backendDrainCompare : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
57field unrestricted backendDrainSubtract : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
58field unrestricted backendDrainAdd : (pi unrestricted left : R . (pi unrestricted right : R . (pi unrestricted tail : A . A)))
59field unrestricted backendDrainAddImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
60field unrestricted backendDrainMultiplyImmediate : (pi unrestricted register : R . (pi unrestricted value : Nat . (pi unrestricted tail : A . A)))
61field unrestricted backendDrainDivide : (pi unrestricted divisor : R . (pi unrestricted tail : A . A))
62field unrestricted backendDrainJumpIf : (pi unrestricted condition : (family TelemetryDrainCondition) . (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)))
63field unrestricted backendDrainJump : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
64field unrestricted backendDrainLabel : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A))
65field unrestricted backendDrainReturn : (pi unrestricted tail : A . A)
66field unrestricted backendDrainEnd : A
67field unrestricted backendDrainResult : R
68field unrestricted backendDrainArgument0 : R
69field unrestricted backendDrainArgument1 : R
70field unrestricted backendDrainArgument2 : R
71field unrestricted backendDrainArgument3 : R
72field unrestricted backendDrainArgument4 : R
73field unrestricted backendDrainArgument5 : R
74field unrestricted backendDrainScratch0 : R
75field unrestricted backendDrainScratch1 : R
76
77end-family
78
79def telemetryDrainAssemblyFor =
80 (lambda erased A : Type 0 .
81 (lambda erased R : Type 0 .
82 (lambda unrestricted backend : (family TelemetryDrainBackend A R) .
83 (lambda unrestricted kind : (family TelemetryDrainRoutineKind) .
84 (eliminate
85 TelemetryDrainBackend
86 (lambda unrestricted current : (family TelemetryDrainBackend A R) . A)
87 backend
88 (branch
89 TelemetryDrainBackendValue
90 drainSet
91 drainMove
92 drainLoad
93 drainStore64
94 drainStore8
95 drainCompareImmediate
96 drainCompare
97 drainSubtract
98 drainAdd
99 drainAddImmediate
100 drainMultiplyImmediate
101 drainDivide
102 drainJumpIf
103 drainJump
104 drainLabel
105 drainReturn
106 drainEnd
107 drainResult
108 drainArgument0
109 drainArgument1
110 drainArgument2
111 drainArgument3
112 drainArgument4
113 drainArgument5
114 drainScratch0
115 drainScratch1
116 .
117 (let unrestricted drainAllowedTagsWith =
118 (lambda unrestricted routes : (family TelemetryRecordRoutes) .
119 (lambda unrestricted tail : A .
120 (eliminate
121 TelemetryRecordRoutes
122 (lambda unrestricted current : (family TelemetryRecordRoutes) . A)
123 routes
124 (branch TelemetryRecordRoutesEnd . (drainJump b"route-read-invalid" tail))
125 (branch
126 TelemetryRecordRoutesNext
127 tag
128 recipe
129 following
130 induction
131 .
132 (drainCompareImmediate
133 drainResult
134 tag
135 (drainJumpIf
136 (constructor TelemetryDrainCondition TelemetryDrainZero)
137 b"route-read-valid"
138 induction))))))
139 in
140 (eliminate
141 TelemetryDrainRoutineKind
142 (lambda unrestricted current : (family TelemetryDrainRoutineKind) . A)
143 kind
144 (branch
145 TelemetryDrainReadyRoutine
146 .
147 (drainLoad
148 drainResult
149 drainArgument0
150 publicationReadyAt
151 (drainCompareImmediate
152 drainResult
153 1
154 (drainJumpIf
155 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
156 b"drain-not-ready"
157 (drainSet
158 drainResult
159 1
160 (drainReturn
161 (drainLabel
162 b"drain-not-ready"
163 (drainSet drainResult 0 (drainReturn drainEnd)))))))))
164 (branch
165 TelemetryDrainAppendRoutine
166 bound
167 .
168 (drainCompareImmediate
169 drainArgument3
170 (publicationArenaBytesForBody bound)
171 (drainJumpIf
172 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
173 b"drain-append-inaccessible"
174 (drainCompareImmediate
175 drainArgument2
176 bound
177 (drainJumpIf
178 (constructor TelemetryDrainCondition TelemetryDrainAbove)
179 b"drain-append-refused"
180 (drainMove
181 drainResult
182 drainArgument2
183 (drainAddImmediate
184 drainResult
185 telemetryRecordAt
186 (drainCompare
187 drainArgument4
188 drainResult
189 (drainJumpIf
190 (constructor TelemetryDrainCondition TelemetryDrainBelow)
191 b"drain-append-refused"
192 (drainLoad
193 drainResult
194 drainArgument0
195 publicationReadyAt
196 (drainCompareImmediate
197 drainResult
198 1
199 (drainJumpIf
200 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
201 b"drain-append-refused"
202 (drainLoad
203 drainResult
204 drainArgument1
205 0
206 (drainCompareImmediate
207 drainResult
208 0
209 (drainJumpIf
210 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
211 b"drain-append-refused"
212 (drainLoad
213 drainResult
214 drainArgument0
215 publicationBodyLengthAt
216 (drainCompareImmediate
217 drainResult
218 publicationPayloadRecordsAt
219 (drainJumpIf
220 (constructor TelemetryDrainCondition TelemetryDrainBelow)
221 b"drain-append-refused"
222 (drainCompareImmediate
223 drainResult
224 bound
225 (drainJumpIf
226 (constructor TelemetryDrainCondition TelemetryDrainAbove)
227 b"drain-append-refused"
228 (drainMove
229 drainScratch0
230 drainResult
231 (drainAdd
232 drainScratch0
233 drainArgument2
234 (drainAddImmediate
235 drainScratch0
236 1
237 (drainCompareImmediate
238 drainScratch0
239 bound
240 (drainJumpIf
241 (constructor TelemetryDrainCondition TelemetryDrainAbove)
242 b"drain-append-refused"
243 (drainMove
244 drainScratch1
245 drainArgument0
246 (drainAddImmediate
247 drainScratch1
248 publicationBodyAt
249 (drainAdd
250 drainScratch1
251 drainResult
252 (drainStore64
253 drainArgument0
254 publicationSavedR12At
255 drainScratch1
256 (drainAdd
257 drainScratch1
258 drainArgument2
259 (drainSet
260 drainResult
261 10
262 (drainStore8
263 drainScratch1
264 0
265 drainResult
266 (drainStore64
267 drainArgument0
268 publicationBodyLengthAt
269 drainScratch0
270 (drainSet
271 drainResult
272 nativeTelemetryEmptyErrorPayloadAt
273 (drainSubtract
274 drainScratch0
275 drainResult
276 (drainStore64
277 drainArgument0
278 (naturalAdd
279 publicationBodyAt
280 nativeTelemetryEmptyErrorPayloadExtentAt)
281 drainScratch0
282 (drainSet
283 drainResult
284 1
285 (drainReturn
286 (drainLabel
287 b"drain-append-refused"
288 (drainSet
289 drainResult
290 0
291 (drainStore64
292 drainArgument0
293 publicationReadyAt
294 drainResult
295 (drainLabel
296 b"drain-append-inaccessible"
297 (drainSet drainResult 0 (drainReturn drainEnd))))))))))))))))))))))))))))))))))))))))))))
298 (branch
299 TelemetryDrainCommitTagRoutine
300 ordinaryCapacity
301 reservedCapacity
302 role
303 tag
304 .
305 (drainCompareImmediate
306 drainArgument2
307 4
308 (drainJumpIf
309 (constructor TelemetryDrainCondition TelemetryDrainAbove)
310 b"route-tag-invalid"
311 (drainCompareImmediate
312 drainArgument2
313 1
314 (drainJumpIf
315 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
316 b"route-tag-not-queued"
317 (drainCompareImmediate
318 drainArgument3
319 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity)
320 (drainJumpIf
321 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
322 b"route-tag-invalid"
323 (drainLoad
324 drainResult
325 drainArgument0
326 captureOrdinaryCapacityAt
327 (drainCompareImmediate
328 drainResult
329 ordinaryCapacity
330 (drainJumpIf
331 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
332 b"route-tag-invalid"
333 (drainLoad
334 drainResult
335 drainArgument0
336 captureReservedCapacityAt
337 (drainCompareImmediate
338 drainResult
339 reservedCapacity
340 (drainJumpIf
341 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
342 b"route-tag-invalid"
343 (drainLoad
344 drainResult
345 drainArgument0
346 (aosChoose
347 Nat
348 role
349 captureReservedUsedAt
350 captureOrdinaryUsedAt)
351 (drainCompareImmediate
352 drainResult
353 0
354 (drainJumpIf
355 (constructor TelemetryDrainCondition TelemetryDrainZero)
356 b"route-tag-invalid"
357 (drainCompareImmediate
358 drainResult
359 (aosChoose Nat role reservedCapacity ordinaryCapacity)
360 (drainJumpIf
361 (constructor TelemetryDrainCondition TelemetryDrainAbove)
362 b"route-tag-invalid"
363 (drainSet
364 drainScratch0
365 1
366 (drainSubtract
367 drainResult
368 drainScratch0
369 (drainAddImmediate
370 drainResult
371 (naturalMultiply role ordinaryCapacity)
372 (drainMultiplyImmediate
373 drainResult
374 captureWordBytes
375 (drainAdd
376 drainResult
377 drainArgument1
378 (drainSet
379 drainScratch0
380 tag
381 (drainStore64
382 drainResult
383 0
384 drainScratch0
385 (drainSet
386 drainResult
387 1
388 (drainReturn
389 (drainLabel
390 b"route-tag-invalid"
391 (drainSet
392 drainResult
393 4
394 (drainReturn
395 (drainLabel
396 b"route-tag-not-queued"
397 (drainMove
398 drainResult
399 drainArgument2
400 (drainReturn drainEnd)))))))))))))))))))))))))))))))))
401 (branch
402 TelemetryDrainReadTagRoutine
403 ordinaryCapacity
404 reservedCapacity
405 routes
406 .
407 (drainCompareImmediate
408 drainArgument4
409 (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity)
410 (drainJumpIf
411 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
412 b"route-read-invalid"
413 (drainCompare
414 drainArgument1
415 drainArgument2
416 (drainJumpIf
417 (constructor TelemetryDrainCondition TelemetryDrainBelow)
418 b"route-read-invalid"
419 (drainMove
420 drainResult
421 drainArgument1
422 (drainSubtract
423 drainResult
424 drainArgument2
425 (drainSet
426 drainArgument2
427 0
428 (drainSet
429 drainScratch0
430 captureRecordBytes
431 (drainDivide
432 drainScratch0
433 (drainCompareImmediate
434 drainArgument2
435 0
436 (drainJumpIf
437 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
438 b"route-read-invalid"
439 (drainCompareImmediate
440 drainResult
441 (naturalAdd ordinaryCapacity reservedCapacity)
442 (drainJumpIf
443 (constructor TelemetryDrainCondition TelemetryDrainAbove)
444 b"route-read-invalid"
445 (drainJumpIf
446 (constructor TelemetryDrainCondition TelemetryDrainZero)
447 b"route-read-invalid"
448 (drainMultiplyImmediate
449 drainResult
450 captureWordBytes
451 (drainAdd
452 drainResult
453 drainArgument3
454 (drainLoad
455 drainResult
456 drainResult
457 0
458 (drainAllowedTagsWith
459 routes
460 (drainLabel
461 b"route-read-valid"
462 (drainStore64
463 drainArgument5
464 0
465 drainResult
466 (drainSet
467 drainResult
468 1
469 (drainReturn
470 (drainLabel
471 b"route-read-invalid"
472 (drainSet
473 drainResult
474 0
475 (drainStore64
476 drainArgument0
477 publicationReadyAt
478 drainResult
479 (drainStore64
480 drainArgument5
481 0
482 drainResult
483 (drainReturn drainEnd))))))))))))))))))))))))))))
484 (branch
485 TelemetryDrainMatchTagRoutine
486 tag
487 .
488 (drainLoad
489 drainResult
490 drainArgument0
491 0
492 (drainCompareImmediate
493 drainResult
494 tag
495 (drainJumpIf
496 (constructor TelemetryDrainCondition TelemetryDrainNotZero)
497 b"route-unmatched"
498 (drainSet
499 drainResult
500 1
501 (drainReturn
502 (drainLabel
503 b"route-unmatched"
504 (drainSet drainResult 0 (drainReturn drainEnd)))))))))))))))))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.