1module Runtime.TelemetryCaptureRoutine
2
3import Runtime.TelemetryCapture
4import Std.Natural
5
6-- One bounded, single-writer acquisition algorithm. The host emitter owns its
7-- calling convention; this algorithm neither allocates nor performs IO.
8-- Loads/stores are little-endian 64-bit words and arithmetic wraps at 64 bits.
9-- Compare supplies unsigned order/equality. Add must also supply Below iff its
10-- unsigned sum overflowed; no other Add flags are used. CompareMaximum tests
11-- against the full unsigned 64-bit maximum, independent of ISA immediates.
12-- Product multiplies ProductLow by Position, replacing ProductLow with the
13-- low word and ValuesOrOverflow with zero iff the full product fits a word.
14-- SavedValues preserves the original values pointer across that check. No
15-- caller state is mutated before all extent and counter checks have succeeded.
16-- Scale multiplies by the positive record stride with word-wrap semantics.
17family TelemetryCaptureCondition : Type 0
18constructor TelemetryCaptureZero
19constructor TelemetryCaptureNotZero
20constructor TelemetryCaptureBelow
21constructor TelemetryCaptureAbove
22
23end-family
24
25family TelemetryCaptureBackend : Type 0
26parameter erased A : Type 0
27parameter erased R : Type 0
28constructor TelemetryCaptureBackendValue
29field unrestricted backendCaptureLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A))))
30field unrestricted backendCaptureStore : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A))))
31field unrestricted backendCaptureMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
32field unrestricted backendCaptureAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
33field unrestricted backendCaptureCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
34field unrestricted backendCaptureCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
35field unrestricted backendCaptureCompareMaximum : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A))
36field unrestricted backendCaptureSet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
37field unrestricted backendCaptureIncrement : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A))
38field unrestricted backendCaptureScale : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
39field unrestricted backendCaptureProduct : (pi unrestricted a0 : A . A)
40field unrestricted backendCaptureReturnCode : (pi unrestricted a0 : Nat . (pi unrestricted a1 : A . A))
41field unrestricted backendCaptureLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
42field unrestricted backendCaptureJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
43field unrestricted backendCaptureJumpIf : (pi unrestricted a0 : (family TelemetryCaptureCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A)))
44field unrestricted backendCaptureEnd : A
45field unrestricted backendCaptureProductLow : R
46field unrestricted backendCaptureSelected : R
47field unrestricted backendCaptureValuesOrOverflow : R
48field unrestricted backendCaptureQueue : R
49field unrestricted backendCaptureControl : R
50field unrestricted backendCaptureReserved : R
51field unrestricted backendCaptureQueueExtent : R
52field unrestricted backendCapturePosition : R
53field unrestricted backendCaptureSavedValues : R
54
55end-family
56
57def telemetryCaptureAssemblyFor =
58 (lambda erased A : Type 0 .
59 (lambda erased R : Type 0 .
60 (lambda unrestricted backend : (family TelemetryCaptureBackend A R) .
61 (eliminate
62 TelemetryCaptureBackend
63 (lambda unrestricted current : (family TelemetryCaptureBackend A R) . A)
64 backend
65 (branch
66 TelemetryCaptureBackendValue
67 captureLoad
68 captureStore
69 captureMove
70 captureAdd
71 captureCompare
72 captureCompareImmediate
73 captureCompareMaximum
74 captureSet
75 captureIncrement
76 captureScale
77 captureProduct
78 captureReturnCode
79 captureLabel
80 captureJump
81 captureJumpIf
82 captureEnd
83 captureProductLow
84 captureSelected
85 captureValuesOrOverflow
86 captureQueue
87 captureControl
88 captureReserved
89 captureQueueExtent
90 capturePosition
91 captureSavedValues
92 .
93 (let unrestricted captureCopyValues =
94 (lambda unrestricted words : Nat .
95 (lambda unrestricted tail : A .
96 (nat-eliminate
97 (lambda unrestricted n : Nat . A)
98 tail
99 (lambda unrestricted index : Nat .
100 (lambda unrestricted previous : A .
101 (captureLoad
102 captureProductLow
103 captureValuesOrOverflow
104 (naturalMultiply index captureWordBytes)
105 (captureStore
106 capturePosition
107 (naturalAdd captureValuesAt (naturalMultiply index captureWordBytes))
108 captureProductLow
109 previous))))
110 words)))
111 in
112 (let unrestricted captureAssemblyPart4 =
113 (captureLabel b"reject" (captureReturnCode 4 captureEnd))
114 in
115 (let unrestricted captureAssemblyPart3 =
116 (captureJumpIf
117 (constructor TelemetryCaptureCondition TelemetryCaptureNotZero)
118 b"pause"
119 (captureLoad
120 captureProductLow
121 captureControl
122 captureNextSequenceAt
123 (captureCompareMaximum
124 captureProductLow
125 (captureJumpIf
126 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
127 b"reject"
128 (captureMove
129 capturePosition
130 captureProductLow
131 (captureLoad
132 captureProductLow
133 captureControl
134 captureDroppedAt
135 (captureCompareMaximum
136 captureProductLow
137 (captureJumpIf
138 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
139 b"reject"
140 (captureIncrement
141 captureProductLow
142 (captureStore
143 captureControl
144 captureDroppedAt
145 captureProductLow
146 (captureIncrement
147 capturePosition
148 (captureStore
149 captureControl
150 captureNextSequenceAt
151 capturePosition
152 (captureReturnCode
153 2
154 (captureLabel
155 b"excluded"
156 (captureCompareImmediate
157 captureReserved
158 0
159 (captureJumpIf
160 (constructor
161 TelemetryCaptureCondition
162 TelemetryCaptureNotZero)
163 b"reject"
164 (captureLoad
165 captureProductLow
166 captureControl
167 captureExcludedAt
168 (captureCompareMaximum
169 captureProductLow
170 (captureJumpIf
171 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
172 b"reject"
173 (captureIncrement
174 captureProductLow
175 (captureStore
176 captureControl
177 captureExcludedAt
178 captureProductLow
179 (captureReturnCode
180 0
181 (captureLabel
182 b"pause"
183 (captureReturnCode 3 captureAssemblyPart4))))))))))))))))))))))))
184 in
185 (let unrestricted captureAssemblyPart2 =
186 (captureAdd
187 capturePosition
188 captureProductLow
189 (captureLoad
190 captureProductLow
191 captureControl
192 captureNextSequenceAt
193 (captureCompareMaximum
194 captureProductLow
195 (captureJumpIf
196 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
197 b"reject"
198 (captureStore
199 capturePosition
200 captureSequenceAt
201 captureProductLow
202 (captureCopyValues
203 captureValueWords
204 (captureLoad
205 captureProductLow
206 captureControl
207 captureNextSequenceAt
208 (captureIncrement
209 captureProductLow
210 (captureStore
211 captureControl
212 captureNextSequenceAt
213 captureProductLow
214 (captureCompareImmediate
215 captureReserved
216 0
217 (captureJumpIf
218 (constructor
219 TelemetryCaptureCondition
220 TelemetryCaptureNotZero)
221 b"commit-reserved"
222 (captureLoad
223 captureProductLow
224 captureControl
225 captureOrdinaryUsedAt
226 (captureIncrement
227 captureProductLow
228 (captureStore
229 captureControl
230 captureOrdinaryUsedAt
231 captureProductLow
232 (captureJump
233 b"queued"
234 (captureLabel
235 b"commit-reserved"
236 (captureLoad
237 captureProductLow
238 captureControl
239 captureReservedUsedAt
240 (captureIncrement
241 captureProductLow
242 (captureStore
243 captureControl
244 captureReservedUsedAt
245 captureProductLow
246 (captureLabel
247 b"queued"
248 (captureReturnCode
249 1
250 (captureLabel
251 b"ordinary-full"
252 (captureLoad
253 captureProductLow
254 captureControl
255 captureRequiredAt
256 (captureCompareImmediate
257 captureProductLow
258 0
259 captureAssemblyPart3))))))))))))))))))))))))
260 in
261 (let unrestricted captureAssemblyPart1 =
262 (captureCompareImmediate
263 captureValuesOrOverflow
264 0
265 (captureJumpIf
266 (constructor TelemetryCaptureCondition TelemetryCaptureNotZero)
267 b"reject"
268 (captureCompare
269 captureProductLow
270 captureQueueExtent
271 (captureJumpIf
272 (constructor TelemetryCaptureCondition TelemetryCaptureAbove)
273 b"reject"
274 (captureMove
275 captureValuesOrOverflow
276 captureSavedValues
277 (captureCompareImmediate
278 captureSelected
279 0
280 (captureJumpIf
281 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
282 b"excluded"
283 (captureCompareImmediate
284 captureReserved
285 0
286 (captureJumpIf
287 (constructor
288 TelemetryCaptureCondition
289 TelemetryCaptureNotZero)
290 b"reserved"
291 (captureLoad
292 captureProductLow
293 captureControl
294 captureOrdinaryUsedAt
295 (captureLoad
296 capturePosition
297 captureControl
298 captureOrdinaryCapacityAt
299 (captureCompare
300 captureProductLow
301 capturePosition
302 (captureJumpIf
303 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
304 b"ordinary-full"
305 (captureJump
306 b"position"
307 (captureLabel
308 b"reserved"
309 (captureLoad
310 captureProductLow
311 captureControl
312 captureReservedUsedAt
313 (captureLoad
314 capturePosition
315 captureControl
316 captureReservedCapacityAt
317 (captureCompare
318 captureProductLow
319 capturePosition
320 (captureJumpIf
321 (constructor TelemetryCaptureCondition TelemetryCaptureZero)
322 b"pause"
323 (captureLoad
324 capturePosition
325 captureControl
326 captureOrdinaryCapacityAt
327 (captureAdd
328 captureProductLow
329 capturePosition
330 (captureLabel
331 b"position"
332 (captureScale
333 captureProductLow
334 captureRecordBytes
335 (captureMove
336 capturePosition
337 captureQueue
338 captureAssemblyPart2))))))))))))))))))))))))
339 in
340 (let unrestricted captureAssemblyPart0 =
341 (captureMove
342 captureSavedValues
343 captureValuesOrOverflow
344 (captureCompareImmediate
345 captureSelected
346 1
347 (captureJumpIf
348 (constructor TelemetryCaptureCondition TelemetryCaptureAbove)
349 b"reject"
350 (captureCompareImmediate
351 captureReserved
352 1
353 (captureJumpIf
354 (constructor TelemetryCaptureCondition TelemetryCaptureAbove)
355 b"reject"
356 (captureLoad
357 captureProductLow
358 captureControl
359 captureRequiredAt
360 (captureCompareImmediate
361 captureProductLow
362 1
363 (captureJumpIf
364 (constructor
365 TelemetryCaptureCondition
366 TelemetryCaptureAbove)
367 b"reject"
368 (captureLoad
369 captureProductLow
370 captureControl
371 captureOrdinaryUsedAt
372 (captureLoad
373 capturePosition
374 captureControl
375 captureOrdinaryCapacityAt
376 (captureCompare
377 captureProductLow
378 capturePosition
379 (captureJumpIf
380 (constructor
381 TelemetryCaptureCondition
382 TelemetryCaptureAbove)
383 b"reject"
384 (captureLoad
385 captureProductLow
386 captureControl
387 captureReservedUsedAt
388 (captureLoad
389 capturePosition
390 captureControl
391 captureReservedCapacityAt
392 (captureCompare
393 captureProductLow
394 capturePosition
395 (captureJumpIf
396 (constructor
397 TelemetryCaptureCondition
398 TelemetryCaptureAbove)
399 b"reject"
400 (captureLoad
401 captureProductLow
402 captureControl
403 captureOrdinaryCapacityAt
404 (captureLoad
405 capturePosition
406 captureControl
407 captureReservedCapacityAt
408 (captureCompareImmediate
409 capturePosition
410 2
411 (captureJumpIf
412 (constructor
413 TelemetryCaptureCondition
414 TelemetryCaptureBelow)
415 b"reject"
416 (captureAdd
417 captureProductLow
418 capturePosition
419 (captureJumpIf
420 (constructor
421 TelemetryCaptureCondition
422 TelemetryCaptureBelow)
423 b"reject"
424 (captureSet
425 capturePosition
426 captureRecordBytes
427 (captureProduct captureAssemblyPart1))))))))))))))))))))))))
428 in
429 captureAssemblyPart0)))))))))))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.