1module Runtime.TelemetryValueRoutine
2
3import Observe.Value
4import Runtime.TelemetryCapture
5import Runtime.TelemetryValue
6import Std.Natural
7
8-- One bounded decimal/hex algorithm, instantiated with host instruction
9-- emitters. Word operations wrap at 64 bits; byte loads zero-extend and byte
10-- stores truncate. Compare is unsigned. AddImmediate sign-extends its 32-bit
11-- operand, including the decrement; shifts are logical. Divide consumes Result
12-- with zero RemainderOrExtent, yields quotient/remainder in those roles and
13-- requires a positive divisor (the decimal algorithm uses ten). All extent
14-- refusal branches precede source loads or destination writes. Pointer validity
15-- and disjoint buffers remain caller arena obligations, not an entropy or
16-- durability claim. Emitters preserve their interpreter's persistent state.
17-- Direct decimal uses Input as a word and RemainderOrExtent as destination
18-- capacity. Hex/word/slice use Input as a pointer, RemainderOrExtent as source
19-- capacity and Counter as destination capacity. Adapters check both ranges
20-- before replacing those roles with the direct decimal ABI. Hex branch names
21-- include byte and nibble position so specialization cannot duplicate labels.
22-- There is no IO, allocation, clock acquisition or acquisition-state mutation.
23family TelemetryValueCondition : Type 0
24constructor TelemetryValueZero
25constructor TelemetryValueNotZero
26constructor TelemetryValueBelow
27constructor TelemetryValueAbove
28
29end-family
30
31family TelemetryValueRoutineKind : Type 0
32constructor TelemetryValueDecimalRoutine
33field unrestricted valueDecimalRoutineSigned : Nat
34constructor TelemetryValueHexRoutine
35field unrestricted valueHexRoutineWidth : Nat
36field unrestricted valueHexRoutineReverse : Nat
37constructor TelemetryValueWordRoutine
38field unrestricted valueWordRoutineSigned : Nat
39field unrestricted valueWordRoutineOffset : Nat
40constructor TelemetryValueSliceRoutine
41field unrestricted valueSliceRoutineWidth : Nat
42field unrestricted valueSliceRoutineReverse : Nat
43field unrestricted valueSliceRoutineOffset : Nat
44
45end-family
46
47family TelemetryValueBackend : Type 0
48parameter erased A : Type 0
49parameter erased R : Type 0
50constructor TelemetryValueBackendValue
51field unrestricted backendValueLoad64 : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A))))
52field unrestricted backendValueLoad8 : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : Nat . (pi unrestricted a3 : A . A))))
53field unrestricted backendValueStore8 : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : R . (pi unrestricted a3 : A . A))))
54field unrestricted backendValueMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
55field unrestricted backendValueSet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
56field unrestricted backendValueCompareImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
57field unrestricted backendValueCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
58field unrestricted backendValueAdd : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
59field unrestricted backendValueAddImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
60field unrestricted backendValueSubtract : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
61field unrestricted backendValueShiftRight : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
62field unrestricted backendValueAndImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
63field unrestricted backendValueDivide : (pi unrestricted a0 : R . (pi unrestricted a1 : A . A))
64field unrestricted backendValueJumpIf : (pi unrestricted a0 : (family TelemetryValueCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A)))
65field unrestricted backendValueJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
66field unrestricted backendValueLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
67field unrestricted backendValueReturn : (pi unrestricted a0 : A . A)
68field unrestricted backendValueEnd : A
69field unrestricted backendValueResult : R
70field unrestricted backendValueInput : R
71field unrestricted backendValueDestination : R
72field unrestricted backendValueRemainderOrExtent : R
73field unrestricted backendValueCounter : R
74field unrestricted backendValueDivisor : R
75field unrestricted backendValueSourceCursor : R
76field unrestricted backendValueDestinationCursor : R
77field unrestricted backendValueNegative : R
78
79end-family
80
81def telemetryValueAssemblyFor =
82 (lambda erased A : Type 0 .
83 (lambda erased R : Type 0 .
84 (lambda unrestricted backend : (family TelemetryValueBackend A R) .
85 (lambda unrestricted kind : (family TelemetryValueRoutineKind) .
86 (eliminate
87 TelemetryValueBackend
88 (lambda unrestricted current : (family TelemetryValueBackend A R) . A)
89 backend
90 (branch
91 TelemetryValueBackendValue
92 valueLoad64
93 valueLoad8
94 valueStore8
95 valueMove
96 valueSet
97 valueCompareImmediate
98 valueCompare
99 valueAdd
100 valueAddImmediate
101 valueSubtract
102 valueShiftRight
103 valueAndImmediate
104 valueDivide
105 valueJumpIf
106 valueJump
107 valueLabel
108 valueReturn
109 valueEnd
110 valueResult
111 valueInput
112 valueDestination
113 valueRemainderOrExtent
114 valueCounter
115 valueDivisor
116 valueSourceCursor
117 valueDestinationCursor
118 valueNegative
119 .
120 (let unrestricted cellDecimalFinish =
121 (valueLabel
122 b"cell-space"
123 (valueCompare
124 valueDestinationCursor
125 valueSourceCursor
126 (valueJumpIf
127 (constructor TelemetryValueCondition TelemetryValueZero)
128 b"cell-complete"
129 (valueSet
130 valueResult
131 32
132 (valueStore8
133 valueDestinationCursor
134 0
135 valueResult
136 (valueAddImmediate
137 valueDestinationCursor
138 1
139 (valueJump
140 b"cell-space"
141 (valueLabel
142 b"cell-complete"
143 (valueSet
144 valueResult
145 34
146 (valueStore8
147 valueDestination
148 0
149 valueResult
150 (valueSet
151 valueResult
152 0
153 (valueReturn
154 (valueLabel
155 b"cell-refused"
156 (valueSet valueResult 4 (valueReturn valueEnd)))))))))))))))
157 in
158 (let unrestricted cellDecimalCopy =
159 (valueMove
160 valueSourceCursor
161 valueDestination
162 (valueAdd
163 valueSourceCursor
164 valueCounter
165 (valueAddImmediate
166 valueSourceCursor
167 1
168 (valueMove
169 valueDestinationCursor
170 valueDestination
171 (valueAddImmediate
172 valueDestinationCursor
173 1
174 (valueCompareImmediate
175 valueNegative
176 0
177 (valueJumpIf
178 (constructor TelemetryValueCondition TelemetryValueZero)
179 b"cell-positive"
180 (valueSet
181 valueResult
182 45
183 (valueStore8
184 valueDestinationCursor
185 0
186 valueResult
187 (valueAddImmediate
188 valueDestinationCursor
189 1
190 (valueLabel
191 b"cell-positive"
192 (valueSet
193 valueDivisor
194 telemetryDecimalDigits
195 (valueSubtract
196 valueDivisor
197 valueCounter
198 (valueLabel
199 b"cell-copy"
200 (valueLoad8
201 valueResult
202 valueSourceCursor
203 0
204 (valueStore8
205 valueDestinationCursor
206 0
207 valueResult
208 (valueAddImmediate
209 valueSourceCursor
210 1
211 (valueAddImmediate
212 valueDestinationCursor
213 1
214 (valueAddImmediate
215 valueDivisor
216 0xffffffff
217 (valueCompareImmediate
218 valueDivisor
219 0
220 (valueJumpIf
221 (constructor TelemetryValueCondition TelemetryValueNotZero)
222 b"cell-copy"
223 (valueSet
224 valueResult
225 34
226 (valueStore8
227 valueDestinationCursor
228 0
229 valueResult
230 (valueAddImmediate
231 valueDestinationCursor
232 1
233 (valueMove
234 valueSourceCursor
235 valueDestination
236 (valueAddImmediate
237 valueSourceCursor
238 telemetryDecimalCellBytes
239 cellDecimalFinish))))))))))))))))))))))))))
240 in
241 (let unrestricted cellDecimalDigits =
242 (valueSet
243 valueCounter
244 telemetryDecimalDigits
245 (valueSet
246 valueDivisor
247 10
248 (valueLabel
249 b"cell-digit"
250 (valueSet
251 valueRemainderOrExtent
252 0
253 (valueDivide
254 valueDivisor
255 (valueAddImmediate
256 valueRemainderOrExtent
257 48
258 (valueMove
259 valueSourceCursor
260 valueDestination
261 (valueAdd
262 valueSourceCursor
263 valueCounter
264 (valueStore8
265 valueSourceCursor
266 0
267 valueRemainderOrExtent
268 (valueAddImmediate
269 valueCounter
270 0xffffffff
271 (valueCompareImmediate
272 valueResult
273 0
274 (valueJumpIf
275 (constructor TelemetryValueCondition TelemetryValueNotZero)
276 b"cell-digit"
277 cellDecimalCopy))))))))))))
278 in
279 (let unrestricted cellDecimalAssembly =
280 (lambda unrestricted signed : Nat .
281 (valueCompareImmediate
282 valueRemainderOrExtent
283 telemetryDecimalCellBytes
284 (valueJumpIf
285 (constructor TelemetryValueCondition TelemetryValueBelow)
286 b"cell-refused"
287 (valueMove
288 valueResult
289 valueInput
290 (valueSet
291 valueNegative
292 0
293 (aosChoose
294 A
295 signed
296 (valueMove
297 valueNegative
298 valueInput
299 (valueShiftRight
300 valueNegative
301 63
302 (valueCompareImmediate
303 valueNegative
304 0
305 (valueJumpIf
306 (constructor TelemetryValueCondition TelemetryValueZero)
307 b"cell-magnitude"
308 (valueSet
309 valueResult
310 0
311 (valueSubtract
312 valueResult
313 valueInput
314 (valueLabel b"cell-magnitude" cellDecimalDigits)))))))
315 cellDecimalDigits))))))
316 in
317 (let unrestricted cellHexNibble =
318 (lambda unrestricted name : Bytes .
319 (lambda unrestricted offset : Nat .
320 (lambda unrestricted tail : A .
321 (valueCompareImmediate
322 valueResult
323 9
324 (valueJumpIf
325 (constructor TelemetryValueCondition TelemetryValueAbove)
326 (bytes-append name b"-letter")
327 (valueAddImmediate
328 valueResult
329 48
330 (valueJump
331 (bytes-append name b"-store")
332 (valueLabel
333 (bytes-append name b"-letter")
334 (valueAddImmediate
335 valueResult
336 87
337 (valueLabel
338 (bytes-append name b"-store")
339 (valueStore8 valueDestination offset valueResult tail)))))))))))
340 in
341 (let unrestricted cellHexByte =
342 (lambda unrestricted source : Nat .
343 (lambda unrestricted index : Nat .
344 (lambda unrestricted tail : A .
345 (let unrestricted destination =
346 (naturalAdd 1 (naturalMultiply 2 index))
347 in
348 (let unrestricted name =
349 (naturalDecimalBytesWithin 20 index)
350 in
351 (valueLoad8
352 valueResult
353 valueInput
354 source
355 (valueShiftRight
356 valueResult
357 4
358 (cellHexNibble
359 (bytes-append name b"-high")
360 destination
361 (valueLoad8
362 valueResult
363 valueInput
364 source
365 (valueAndImmediate
366 valueResult
367 15
368 (cellHexNibble
369 (bytes-append name b"-low")
370 (succ destination)
371 tail)))))))))))
372 in
373 (let unrestricted cellHexAssembly =
374 (lambda unrestricted width : Nat .
375 (lambda unrestricted reverse : Nat .
376 (valueCompareImmediate
377 valueRemainderOrExtent
378 width
379 (valueJumpIf
380 (constructor TelemetryValueCondition TelemetryValueBelow)
381 b"cell-hex-refused"
382 (valueCompareImmediate
383 valueCounter
384 (telemetryHexCellBytes width)
385 (valueJumpIf
386 (constructor TelemetryValueCondition TelemetryValueBelow)
387 b"cell-hex-refused"
388 (nat-eliminate
389 (lambda unrestricted current : Nat . A)
390 (valueSet
391 valueResult
392 34
393 (valueStore8
394 valueDestination
395 0
396 valueResult
397 (valueStore8
398 valueDestination
399 (naturalAdd 1 (naturalMultiply 2 width))
400 valueResult
401 (valueSet
402 valueResult
403 0
404 (valueReturn
405 (valueLabel
406 b"cell-hex-refused"
407 (valueSet valueResult 4 (valueReturn valueEnd))))))))
408 (lambda unrestricted index : Nat .
409 (lambda unrestricted induction : A .
410 (cellHexByte
411 (aosChoose
412 Nat
413 reverse
414 (naturalSaturatingSubtract width (succ index))
415 index)
416 index
417 induction)))
418 width)))))))
419 in
420 (eliminate
421 TelemetryValueRoutineKind
422 (lambda unrestricted current : (family TelemetryValueRoutineKind) . A)
423 kind
424 (branch
425 TelemetryValueDecimalRoutine
426 signed
427 .
428 (cellDecimalAssembly signed))
429 (branch
430 TelemetryValueHexRoutine
431 width
432 reverse
433 .
434 (cellHexAssembly width reverse))
435 (branch
436 TelemetryValueWordRoutine
437 signed
438 offset
439 .
440 (valueCompareImmediate
441 valueRemainderOrExtent
442 (naturalAdd offset captureWordBytes)
443 (valueJumpIf
444 (constructor TelemetryValueCondition TelemetryValueBelow)
445 b"cell-refused"
446 (valueCompareImmediate
447 valueCounter
448 telemetryDecimalCellBytes
449 (valueJumpIf
450 (constructor TelemetryValueCondition TelemetryValueBelow)
451 b"cell-refused"
452 (valueLoad64
453 valueInput
454 valueInput
455 offset
456 (valueMove
457 valueRemainderOrExtent
458 valueCounter
459 (cellDecimalAssembly signed))))))))
460 (branch
461 TelemetryValueSliceRoutine
462 width
463 reverse
464 offset
465 .
466 (valueCompareImmediate
467 valueRemainderOrExtent
468 (naturalAdd offset width)
469 (valueJumpIf
470 (constructor TelemetryValueCondition TelemetryValueBelow)
471 b"cell-hex-refused"
472 (valueCompareImmediate
473 valueCounter
474 (telemetryHexCellBytes width)
475 (valueJumpIf
476 (constructor TelemetryValueCondition TelemetryValueBelow)
477 b"cell-hex-refused"
478 (valueAddImmediate
479 valueInput
480 offset
481 (cellHexAssembly width reverse)))))))))))))))))))))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.