1module Runtime.NativeTelemetry
2
3import Data.SHA256Digest
4import Model.Config
5import Model.Parameter
6import Model.Word32
7import Model.Word64
8import Runtime.LinuxSyscall
9import Std.Natural
10
11family NativeTelemetryErrorCode : Type 0
12constructor NativeTelemetryIdentityInvalid
13constructor NativeTelemetryCounterOverflow
14constructor NativeTelemetryErrorLengthOverflow
15constructor NativeTelemetryPayloadLengthOverflow
16constructor NativeTelemetryPathEmpty
17constructor NativeTelemetryRecordEmpty
18constructor NativeTelemetryOpenFailed
19constructor NativeTelemetryWriteFailed
20constructor NativeTelemetryWriteShort
21constructor NativeTelemetrySyncFailed
22constructor NativeTelemetryCloseFailed
23constructor NativeTelemetryUnexpectedResponse
24constructor NativeTelemetryTerminalStateReused
25constructor NativeTelemetryHostFallbackObserved
26
27end-family
28
29family NativeTelemetryCounterResult : Type 0
30constructor NativeTelemetryCounterSucceeded
31field unrestricted nativeTelemetryCounterValue : (family ModelWord64)
32constructor NativeTelemetryCounterFailed
33field unrestricted nativeTelemetryCounterError : (family NativeTelemetryErrorCode)
34field unrestricted nativeTelemetryCounterNatural : Nat
35
36end-family
37
38family NativeTelemetryCounters : Type 0
39constructor NativeTelemetryCountersValue
40field unrestricted nativeTelemetryCounter0 : (family ModelWord64)
41field unrestricted nativeTelemetryCounter1 : (family ModelWord64)
42field unrestricted nativeTelemetryCounter2 : (family ModelWord64)
43field unrestricted nativeTelemetryCounter3 : (family ModelWord64)
44field unrestricted nativeTelemetryCounter4 : (family ModelWord64)
45field unrestricted nativeTelemetryCounter5 : (family ModelWord64)
46field unrestricted nativeTelemetryCounter6 : (family ModelWord64)
47field unrestricted nativeTelemetryCounter7 : (family ModelWord64)
48
49end-family
50
51family NativeTelemetryRecordRequest : Type 0
52constructor NativeTelemetryRecordRequestValue
53field unrestricted nativeTelemetryRequestSequence : (family ModelWord64)
54field unrestricted nativeTelemetryRequestMonotonicNanoseconds : (family ModelWord64)
55field unrestricted nativeTelemetryRequestDomain : Byte
56field unrestricted nativeTelemetryRequestEvent : Byte
57field unrestricted nativeTelemetryRequestPhase : Byte
58field unrestricted nativeTelemetryRequestStatus : Byte
59field unrestricted nativeTelemetryRequestCounters : (family NativeTelemetryCounters)
60field unrestricted nativeTelemetryRequestIdentity : Bytes
61field unrestricted nativeTelemetryRequestErrorCode : Bytes
62field unrestricted nativeTelemetryRequestPayload : Bytes
63
64end-family
65
66family NativeTelemetryEncodeTelemetry : Type 0
67constructor NativeTelemetryEncodeTelemetryValue
68field unrestricted nativeTelemetryEncodedRecords : Nat
69field unrestricted nativeTelemetryEncodedBodyBytes : Nat
70field unrestricted nativeTelemetryEncodedOutputBytes : Nat
71field unrestricted nativeTelemetryIdentityRejections : Nat
72field unrestricted nativeTelemetryLengthRejections : Nat
73field unrestricted nativeTelemetryEncodingFailures : Nat
74field unrestricted nativeTelemetryEncodingHostFallbacks : Nat
75
76end-family
77
78family NativeTelemetryEncodedRecord : Type 0
79constructor NativeTelemetryEncodedRecordValue
80field unrestricted nativeTelemetryEncodedBytes : Bytes
81field unrestricted nativeTelemetryEncodedExtent : (family ModelWord64)
82field unrestricted nativeTelemetryEncodedSHA256 : Bytes
83field unrestricted nativeTelemetryEncodedIdentity : Bytes
84
85end-family
86
87family NativeTelemetryEncodeResult : Type 0
88constructor NativeTelemetryEncodeSucceeded
89field unrestricted nativeTelemetryEncodeRecord : (family NativeTelemetryEncodedRecord)
90field unrestricted nativeTelemetryEncodeSuccessTelemetry : (family NativeTelemetryEncodeTelemetry)
91constructor NativeTelemetryEncodeFailed
92field unrestricted nativeTelemetryEncodeError : (family NativeTelemetryErrorCode)
93field unrestricted nativeTelemetryEncodeFailureTelemetry : (family NativeTelemetryEncodeTelemetry)
94
95end-family
96
97family NativeTelemetrySinkPhase : Type 0
98constructor NativeTelemetrySinkOpening
99constructor NativeTelemetrySinkWriting
100constructor NativeTelemetrySinkSyncing
101constructor NativeTelemetrySinkClosing
102constructor NativeTelemetrySinkComplete
103constructor NativeTelemetrySinkFailed
104
105end-family
106
107family NativeTelemetryOptionalDescriptor : Type 0
108constructor NativeTelemetryNoDescriptor
109constructor NativeTelemetrySomeDescriptor
110field unrestricted nativeTelemetrySomeDescriptorValue : (family LinuxFileDescriptor)
111
112end-family
113
114family NativeTelemetrySinkTelemetry : Type 0
115constructor NativeTelemetrySinkTelemetryValue
116field unrestricted nativeTelemetrySinkSyscallsPlanned : Nat
117field unrestricted nativeTelemetrySinkSyscallsCompleted : Nat
118field unrestricted nativeTelemetrySinkBytesPlanned : (family ModelWord64)
119field unrestricted nativeTelemetrySinkBytesWritten : (family ModelWord64)
120field unrestricted nativeTelemetrySinkSyncs : Nat
121field unrestricted nativeTelemetrySinkCloses : Nat
122field unrestricted nativeTelemetrySinkFailures : Nat
123field unrestricted nativeTelemetrySinkHostFallbacks : Nat
124
125end-family
126
127family NativeTelemetrySinkState : Type 0
128constructor NativeTelemetrySinkStateValue
129field unrestricted nativeTelemetrySinkPath : Bytes
130field unrestricted nativeTelemetrySinkRecord : (family NativeTelemetryEncodedRecord)
131field unrestricted nativeTelemetrySinkPhaseValue : (family NativeTelemetrySinkPhase)
132field unrestricted nativeTelemetrySinkDescriptor : (family NativeTelemetryOptionalDescriptor)
133field unrestricted nativeTelemetrySinkTelemetryValue : (family NativeTelemetrySinkTelemetry)
134
135end-family
136
137family NativeTelemetrySinkAction : Type 0
138constructor NativeTelemetrySinkIssueSyscall
139field unrestricted nativeTelemetrySinkSyscallRequest : (family LinuxSyscallRequest)
140
141end-family
142
143family NativeTelemetrySinkDecision : Type 0
144constructor NativeTelemetrySinkContinue
145field unrestricted nativeTelemetrySinkContinueState : (family NativeTelemetrySinkState)
146field unrestricted nativeTelemetrySinkContinueAction : (family NativeTelemetrySinkAction)
147constructor NativeTelemetrySinkFinished
148field unrestricted nativeTelemetrySinkFinishedRecord : (family NativeTelemetryEncodedRecord)
149field unrestricted nativeTelemetrySinkFinishedTelemetry : (family NativeTelemetrySinkTelemetry)
150constructor NativeTelemetrySinkRejected
151field unrestricted nativeTelemetrySinkRejectedCode : (family NativeTelemetryErrorCode)
152field unrestricted nativeTelemetrySinkRejectedState : (family NativeTelemetrySinkState)
153
154end-family
155
156def nativeTelemetryErrorCodeBytes =
157 (lambda unrestricted code : (family NativeTelemetryErrorCode) .
158 (eliminate
159 NativeTelemetryErrorCode
160 (lambda unrestricted current : (family NativeTelemetryErrorCode) . Bytes)
161 code
162 (branch NativeTelemetryIdentityInvalid . b"ALPHA-TEL-001")
163 (branch NativeTelemetryCounterOverflow . b"ALPHA-TEL-002")
164 (branch NativeTelemetryErrorLengthOverflow . b"ALPHA-TEL-003")
165 (branch NativeTelemetryPayloadLengthOverflow . b"ALPHA-TEL-004")
166 (branch NativeTelemetryPathEmpty . b"ALPHA-TEL-005")
167 (branch NativeTelemetryRecordEmpty . b"ALPHA-TEL-006")
168 (branch NativeTelemetryOpenFailed . b"ALPHA-TEL-007")
169 (branch NativeTelemetryWriteFailed . b"ALPHA-TEL-008")
170 (branch NativeTelemetryWriteShort . b"ALPHA-TEL-009")
171 (branch NativeTelemetrySyncFailed . b"ALPHA-TEL-010")
172 (branch NativeTelemetryCloseFailed . b"ALPHA-TEL-011")
173 (branch NativeTelemetryUnexpectedResponse . b"ALPHA-TEL-012")
174 (branch NativeTelemetryTerminalStateReused . b"ALPHA-TEL-013")
175 (branch NativeTelemetryHostFallbackObserved . b"ALPHA-TEL-014")))
176
177def nativeTelemetryMagic : Bytes =
178 b"ALPHATEL"
179
180def nativeTelemetryVersion : Byte =
181 (byte 1)
182
183def nativeTelemetryDigestBytes : Nat =
184 (byte-to-nat (byte 64))
185
186def nativeTelemetryZeroWord64 : (family ModelWord64) =
187 0
188
189def nativeTelemetryWord32ToWord64 =
190 (lambda unrestricted value : (family ModelWord32) .
191 (eliminate
192 ModelWord32
193 (lambda unrestricted current : (family ModelWord32) . (family ModelWord64))
194 value
195 (branch
196 ModelWord32Value
197 byte0
198 byte1
199 byte2
200 byte3
201 .
202 (constructor
203 ModelWord64
204 ModelWord64Value
205 byte0
206 byte1
207 byte2
208 byte3
209 (byte 0)
210 (byte 0)
211 (byte 0)
212 (byte 0)))))
213
214def nativeTelemetryWord32Bytes =
215 (lambda unrestricted value : (family ModelWord32) .
216 (eliminate
217 ModelWord32
218 (lambda unrestricted current : (family ModelWord32) . Bytes)
219 value
220 (branch
221 ModelWord32Value
222 byte0
223 byte1
224 byte2
225 byte3
226 .
227 (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))
228
229def nativeTelemetryWord64Bytes =
230 (lambda unrestricted value : (family ModelWord64) .
231 (eliminate
232 ModelWord64
233 (lambda unrestricted current : (family ModelWord64) . Bytes)
234 value
235 (branch
236 ModelWord64Value
237 byte0
238 byte1
239 byte2
240 byte3
241 byte4
242 byte5
243 byte6
244 byte7
245 .
246 (bytes-cons
247 byte0
248 (bytes-cons
249 byte1
250 (bytes-cons
251 byte2
252 (bytes-cons
253 byte3
254 (bytes-cons byte4 (bytes-cons byte5 (bytes-cons byte6 (bytes-cons byte7 b"")))))))))))
255
256def nativeTelemetryCounterFromNatural =
257 (lambda unrestricted value : Nat .
258 (app
259 (lambda unrestricted encoded : (family ModelWord32) .
260 (nat-eliminate
261 (lambda unrestricted exact : Nat . (family NativeTelemetryCounterResult))
262 (constructor
263 NativeTelemetryCounterResult
264 NativeTelemetryCounterFailed
265 (constructor NativeTelemetryErrorCode NativeTelemetryCounterOverflow)
266 value)
267 (lambda unrestricted exactPredecessor : Nat .
268 (lambda unrestricted ignoredExact : (family NativeTelemetryCounterResult) .
269 (constructor
270 NativeTelemetryCounterResult
271 NativeTelemetryCounterSucceeded
272 (nativeTelemetryWord32ToWord64 encoded))))
273 (naturalEqual (modelWord32ToNatural encoded) value)))
274 (modelWord32FromNaturalTruncated value)))
275
276def nativeTelemetryEncodeTelemetry =
277 (lambda unrestricted records : Nat .
278 (lambda unrestricted bodyBytes : Nat .
279 (lambda unrestricted outputBytes : Nat .
280 (lambda unrestricted identityRejections : Nat .
281 (lambda unrestricted lengthRejections : Nat .
282 (lambda unrestricted failures : Nat .
283 (constructor
284 NativeTelemetryEncodeTelemetry
285 NativeTelemetryEncodeTelemetryValue
286 records
287 bodyBytes
288 outputBytes
289 identityRejections
290 lengthRejections
291 failures
292 zero)))))))
293
294def nativeTelemetryEncodeFailure =
295 (lambda unrestricted code : (family NativeTelemetryErrorCode) .
296 (lambda unrestricted identityRejections : Nat .
297 (lambda unrestricted lengthRejections : Nat .
298 (constructor
299 NativeTelemetryEncodeResult
300 NativeTelemetryEncodeFailed
301 code
302 (nativeTelemetryEncodeTelemetry
303 zero
304 zero
305 zero
306 identityRejections
307 lengthRejections
308 (succ zero))))))
309
310def nativeTelemetryEncodeCounters =
311 (lambda unrestricted counters : (family NativeTelemetryCounters) .
312 (eliminate
313 NativeTelemetryCounters
314 (lambda unrestricted current : (family NativeTelemetryCounters) . Bytes)
315 counters
316 (branch
317 NativeTelemetryCountersValue
318 counter0
319 counter1
320 counter2
321 counter3
322 counter4
323 counter5
324 counter6
325 counter7
326 .
327 (bytes-builder-build
328 (bytes-builder-append
329 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter0))
330 (bytes-builder-append
331 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter1))
332 (bytes-builder-append
333 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter2))
334 (bytes-builder-append
335 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter3))
336 (bytes-builder-append
337 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter4))
338 (bytes-builder-append
339 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter5))
340 (bytes-builder-append
341 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter6))
342 (bytes-builder-chunk (nativeTelemetryWord64Bytes counter7)))))))))))))
343
344-- Part of `nativeTelemetryBuildRecord`, lifted out to keep it inside the §28.3 size and
345-- nesting limits; the parameters are the locals it still needs.
346def nativeTelemetryBuildRecordPart1 =
347 (lambda unrestricted sequence : (family ModelWord64) .
348 (lambda unrestricted monotonic : (family ModelWord64) .
349 (lambda unrestricted counters : (family NativeTelemetryCounters) .
350 (lambda unrestricted identity : Bytes .
351 (lambda unrestricted errorCode : Bytes .
352 (lambda unrestricted payload : Bytes .
353 (lambda unrestricted errorExtent : (family ModelWord64) .
354 (lambda unrestricted payloadExtent : (family ModelWord64) .
355 (bytes-builder-build
356 (bytes-builder-append
357 (bytes-builder-chunk (nativeTelemetryWord64Bytes sequence))
358 (bytes-builder-append
359 (bytes-builder-chunk (nativeTelemetryWord64Bytes monotonic))
360 (bytes-builder-append
361 (bytes-builder-chunk (nativeTelemetryEncodeCounters counters))
362 (bytes-builder-append
363 (bytes-builder-chunk identity)
364 (bytes-builder-append
365 (bytes-builder-chunk (nativeTelemetryWord64Bytes errorExtent))
366 (bytes-builder-append
367 (bytes-builder-chunk errorCode)
368 (bytes-builder-append
369 (bytes-builder-chunk (nativeTelemetryWord64Bytes payloadExtent))
370 (bytes-builder-chunk payload)))))))))))))))))
371
372-- The record's body -- what its digest covers -- from its fields and the
373-- two extents; `nativeTelemetryBuildRecord` frames it with the magic and
374-- the digest, and an executable that seals a record at run time
375-- (Runtime.NativeTelemetrySeal) starts from it.
376def nativeTelemetryRecordBodyForVersion =
377 (lambda unrestricted version : Byte .
378 (lambda unrestricted sequence : (family ModelWord64) .
379 (lambda unrestricted monotonic : (family ModelWord64) .
380 (lambda unrestricted domain : Byte .
381 (lambda unrestricted event : Byte .
382 (lambda unrestricted phase : Byte .
383 (lambda unrestricted status : Byte .
384 (lambda unrestricted counters : (family NativeTelemetryCounters) .
385 (lambda unrestricted identity : Bytes .
386 (lambda unrestricted errorCode : Bytes .
387 (lambda unrestricted payload : Bytes .
388 (lambda unrestricted errorExtent : (family ModelWord64) .
389 (lambda unrestricted payloadExtent : (family ModelWord64) .
390 (bytes-cons
391 version
392 (bytes-cons
393 domain
394 (bytes-cons
395 event
396 (bytes-cons
397 phase
398 (bytes-cons
399 status
400 (nativeTelemetryBuildRecordPart1
401 sequence
402 monotonic
403 counters
404 identity
405 errorCode
406 payload
407 errorExtent
408 payloadExtent)))))))))))))))))))
409
410-- Version one remains byte-for-byte compatible. Version two uses the same
411-- bounded framing/hash, with producer binding and batch semantics owned by
412-- Runtime.TelemetryPublication; it is not an alternate AOS recorder.
413def nativeTelemetryRecordBody =
414 (nativeTelemetryRecordBodyForVersion nativeTelemetryVersion)
415
416def nativeTelemetryFlagsBytes : Nat =
417 (bytes-length (bytes 1 0 0 0 0))
418
419def nativeTelemetryScalarBytes : Nat =
420 (bytes-length (nativeTelemetryWord64Bytes nativeTelemetryZeroWord64))
421
422def nativeTelemetrySequenceAt : Nat =
423 nativeTelemetryFlagsBytes
424
425def nativeTelemetryMonotonicAt : Nat =
426 (naturalAdd nativeTelemetrySequenceAt nativeTelemetryScalarBytes)
427
428def nativeTelemetryCountersAt : Nat =
429 (naturalAdd nativeTelemetryMonotonicAt nativeTelemetryScalarBytes)
430
431def nativeTelemetryIdentityAt : Nat =
432 (naturalAdd
433 nativeTelemetryCountersAt
434 (bytes-length
435 (nativeTelemetryEncodeCounters
436 (constructor NativeTelemetryCounters NativeTelemetryCountersValue 0 0 0 0 0 0 0 0))))
437
438def nativeTelemetryErrorExtentAt : Nat =
439 (naturalAdd nativeTelemetryIdentityAt nativeTelemetryDigestBytes)
440
441def nativeTelemetryEmptyErrorPayloadExtentAt : Nat =
442 (naturalAdd nativeTelemetryErrorExtentAt nativeTelemetryScalarBytes)
443
444def nativeTelemetryEmptyErrorPayloadAt : Nat =
445 (naturalAdd nativeTelemetryEmptyErrorPayloadExtentAt nativeTelemetryScalarBytes)
446
447def nativeTelemetryBuildRecord =
448 (lambda unrestricted request : (family NativeTelemetryRecordRequest) .
449 (eliminate
450 NativeTelemetryRecordRequest
451 (lambda unrestricted current : (family NativeTelemetryRecordRequest) .
452 (family NativeTelemetryEncodeResult))
453 request
454 (branch
455 NativeTelemetryRecordRequestValue
456 sequence
457 monotonic
458 domain
459 event
460 phase
461 status
462 counters
463 identity
464 errorCode
465 payload
466 .
467 (nat-eliminate
468 (lambda unrestricted identityValid : Nat . (family NativeTelemetryEncodeResult))
469 (nativeTelemetryEncodeFailure
470 (constructor NativeTelemetryErrorCode NativeTelemetryIdentityInvalid)
471 (succ zero)
472 zero)
473 (lambda unrestricted identityPredecessor : Nat .
474 (lambda unrestricted ignoredIdentity : (family NativeTelemetryEncodeResult) .
475 (eliminate
476 NativeTelemetryCounterResult
477 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
478 (family NativeTelemetryEncodeResult))
479 (nativeTelemetryCounterFromNatural (bytes-length errorCode))
480 (branch
481 NativeTelemetryCounterSucceeded
482 errorExtent
483 .
484 (eliminate
485 NativeTelemetryCounterResult
486 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
487 (family NativeTelemetryEncodeResult))
488 (nativeTelemetryCounterFromNatural (bytes-length payload))
489 (branch
490 NativeTelemetryCounterSucceeded
491 payloadExtent
492 .
493 (app
494 (lambda unrestricted body : Bytes .
495 (app
496 (lambda unrestricted output : Bytes .
497 (eliminate
498 NativeTelemetryCounterResult
499 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
500 (family NativeTelemetryEncodeResult))
501 (nativeTelemetryCounterFromNatural (bytes-length output))
502 (branch
503 NativeTelemetryCounterSucceeded
504 outputExtent
505 .
506 (constructor
507 NativeTelemetryEncodeResult
508 NativeTelemetryEncodeSucceeded
509 (constructor
510 NativeTelemetryEncodedRecord
511 NativeTelemetryEncodedRecordValue
512 output
513 outputExtent
514 (sha256HexBytesOrEmpty (sha256Hex body))
515 identity)
516 (nativeTelemetryEncodeTelemetry
517 (succ zero)
518 (bytes-length body)
519 (bytes-length output)
520 zero
521 zero
522 zero)))
523 (branch
524 NativeTelemetryCounterFailed
525 conversionError
526 naturalValue
527 .
528 (nativeTelemetryEncodeFailure
529 (constructor
530 NativeTelemetryErrorCode
531 NativeTelemetryPayloadLengthOverflow)
532 zero
533 (succ zero)))))
534 (bytes-append
535 nativeTelemetryMagic
536 (bytes-append body (sha256HexBytesOrEmpty (sha256Hex body))))))
537 (nativeTelemetryRecordBody
538 sequence
539 monotonic
540 domain
541 event
542 phase
543 status
544 counters
545 identity
546 errorCode
547 payload
548 errorExtent
549 payloadExtent)))
550 (branch
551 NativeTelemetryCounterFailed
552 conversionError
553 naturalValue
554 .
555 (nativeTelemetryEncodeFailure
556 (constructor NativeTelemetryErrorCode NativeTelemetryPayloadLengthOverflow)
557 zero
558 (succ zero)))))
559 (branch
560 NativeTelemetryCounterFailed
561 conversionError
562 naturalValue
563 .
564 (nativeTelemetryEncodeFailure
565 (constructor NativeTelemetryErrorCode NativeTelemetryErrorLengthOverflow)
566 zero
567 (succ zero))))))
568 (naturalEqual (bytes-length identity) nativeTelemetryDigestBytes)))))
569
570def nativeTelemetryAppendFlags : (family ModelWord64) =
571 525377
572
573def nativeTelemetryOwnerReadWriteMode : (family ModelWord64) =
574 384
575
576def nativeTelemetrySinkTelemetryInitial =
577 (lambda unrestricted extent : (family ModelWord64) .
578 (constructor
579 NativeTelemetrySinkTelemetry
580 NativeTelemetrySinkTelemetryValue
581 (succ zero)
582 zero
583 extent
584 nativeTelemetryZeroWord64
585 zero
586 zero
587 zero
588 zero))
589
590def nativeTelemetryOpenAppendRequest =
591 (lambda unrestricted path : Bytes .
592 (constructor
593 LinuxSyscallRequest
594 LinuxOpenAt
595 linuxAtFdcwd
596 path
597 nativeTelemetryAppendFlags
598 nativeTelemetryOwnerReadWriteMode))
599
600def nativeTelemetrySinkBegin =
601 (lambda unrestricted path : Bytes .
602 (lambda unrestricted record : (family NativeTelemetryEncodedRecord) .
603 (eliminate
604 NativeTelemetryEncodedRecord
605 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
606 (family NativeTelemetrySinkDecision))
607 record
608 (branch
609 NativeTelemetryEncodedRecordValue
610 bytes
611 extent
612 digest
613 identity
614 .
615 (app
616 (lambda unrestricted initialState : (family NativeTelemetrySinkState) .
617 (nat-eliminate
618 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
619 (constructor
620 NativeTelemetrySinkDecision
621 NativeTelemetrySinkRejected
622 (constructor NativeTelemetryErrorCode NativeTelemetryPathEmpty)
623 initialState)
624 (lambda unrestricted pathPredecessor : Nat .
625 (lambda unrestricted ignoredPath : (family NativeTelemetrySinkDecision) .
626 (nat-eliminate
627 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
628 (constructor
629 NativeTelemetrySinkDecision
630 NativeTelemetrySinkRejected
631 (constructor NativeTelemetryErrorCode NativeTelemetryRecordEmpty)
632 initialState)
633 (lambda unrestricted recordPredecessor : Nat .
634 (lambda unrestricted ignoredRecord : (family NativeTelemetrySinkDecision) .
635 (constructor
636 NativeTelemetrySinkDecision
637 NativeTelemetrySinkContinue
638 initialState
639 (constructor
640 NativeTelemetrySinkAction
641 NativeTelemetrySinkIssueSyscall
642 (nativeTelemetryOpenAppendRequest path)))))
643 (bytes-length bytes))))
644 (bytes-length path)))
645 (constructor
646 NativeTelemetrySinkState
647 NativeTelemetrySinkStateValue
648 path
649 record
650 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkOpening)
651 (constructor NativeTelemetryOptionalDescriptor NativeTelemetryNoDescriptor)
652 (nativeTelemetrySinkTelemetryInitial extent)))))))
653
654def nativeTelemetrySinkAfterOpen =
655 (lambda unrestricted response : (family LinuxSyscallResponse) .
656 (lambda unrestricted state : (family NativeTelemetrySinkState) .
657 (eliminate
658 LinuxSyscallResponse
659 (lambda unrestricted current : (family LinuxSyscallResponse) .
660 (family NativeTelemetrySinkDecision))
661 response
662 (branch
663 LinuxOpenSucceeded
664 descriptor
665 .
666 (eliminate
667 NativeTelemetrySinkState
668 (lambda unrestricted current : (family NativeTelemetrySinkState) .
669 (family NativeTelemetrySinkDecision))
670 state
671 (branch
672 NativeTelemetrySinkStateValue
673 path
674 record
675 phase
676 oldDescriptor
677 telemetry
678 .
679 (eliminate
680 NativeTelemetryEncodedRecord
681 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
682 (family NativeTelemetrySinkDecision))
683 record
684 (branch
685 NativeTelemetryEncodedRecordValue
686 bytes
687 extent
688 digest
689 identity
690 .
691 (eliminate
692 NativeTelemetrySinkTelemetry
693 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
694 (family NativeTelemetrySinkDecision))
695 telemetry
696 (branch
697 NativeTelemetrySinkTelemetryValue
698 planned
699 completed
700 plannedBytes
701 written
702 syncs
703 closes
704 failures
705 fallbacks
706 .
707 (constructor
708 NativeTelemetrySinkDecision
709 NativeTelemetrySinkContinue
710 (constructor
711 NativeTelemetrySinkState
712 NativeTelemetrySinkStateValue
713 path
714 record
715 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkWriting)
716 (constructor
717 NativeTelemetryOptionalDescriptor
718 NativeTelemetrySomeDescriptor
719 descriptor)
720 (constructor
721 NativeTelemetrySinkTelemetry
722 NativeTelemetrySinkTelemetryValue
723 (succ planned)
724 (succ completed)
725 plannedBytes
726 written
727 syncs
728 closes
729 failures
730 fallbacks))
731 (constructor
732 NativeTelemetrySinkAction
733 NativeTelemetrySinkIssueSyscall
734 (constructor LinuxSyscallRequest LinuxWrite descriptor bytes))))))))))
735 (branch
736 LinuxReadSucceeded
737 bytes
738 .
739 (constructor
740 NativeTelemetrySinkDecision
741 NativeTelemetrySinkRejected
742 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
743 state))
744 (branch
745 LinuxSeekSucceeded
746 position
747 .
748 (constructor
749 NativeTelemetrySinkDecision
750 NativeTelemetrySinkRejected
751 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
752 state))
753 (branch
754 LinuxWriteSucceeded
755 written
756 .
757 (constructor
758 NativeTelemetrySinkDecision
759 NativeTelemetrySinkRejected
760 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
761 state))
762 (branch
763 LinuxIoctlSucceeded
764 output
765 .
766 (constructor
767 NativeTelemetrySinkDecision
768 NativeTelemetrySinkRejected
769 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
770 state))
771 (branch
772 LinuxMmapSucceeded
773 address
774 .
775 (constructor
776 NativeTelemetrySinkDecision
777 NativeTelemetrySinkRejected
778 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
779 state))
780 (branch
781 LinuxUnitSucceeded
782 .
783 (constructor
784 NativeTelemetrySinkDecision
785 NativeTelemetrySinkRejected
786 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
787 state))
788 (branch
789 LinuxSyscallFailed
790 error
791 errno
792 .
793 (constructor
794 NativeTelemetrySinkDecision
795 NativeTelemetrySinkRejected
796 (constructor NativeTelemetryErrorCode NativeTelemetryOpenFailed)
797 state)))))
798
799def nativeTelemetrySinkAfterWrite =
800 (lambda unrestricted response : (family LinuxSyscallResponse) .
801 (lambda unrestricted state : (family NativeTelemetrySinkState) .
802 (eliminate
803 LinuxSyscallResponse
804 (lambda unrestricted current : (family LinuxSyscallResponse) .
805 (family NativeTelemetrySinkDecision))
806 response
807 (branch
808 LinuxOpenSucceeded
809 descriptor
810 .
811 (constructor
812 NativeTelemetrySinkDecision
813 NativeTelemetrySinkRejected
814 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
815 state))
816 (branch
817 LinuxReadSucceeded
818 bytes
819 .
820 (constructor
821 NativeTelemetrySinkDecision
822 NativeTelemetrySinkRejected
823 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
824 state))
825 (branch
826 LinuxSeekSucceeded
827 position
828 .
829 (constructor
830 NativeTelemetrySinkDecision
831 NativeTelemetrySinkRejected
832 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
833 state))
834 (branch
835 LinuxWriteSucceeded
836 written
837 .
838 (eliminate
839 NativeTelemetrySinkState
840 (lambda unrestricted current : (family NativeTelemetrySinkState) .
841 (family NativeTelemetrySinkDecision))
842 state
843 (branch
844 NativeTelemetrySinkStateValue
845 path
846 record
847 phase
848 optionalDescriptor
849 telemetry
850 .
851 (eliminate
852 NativeTelemetryOptionalDescriptor
853 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
854 (family NativeTelemetrySinkDecision))
855 optionalDescriptor
856 (branch
857 NativeTelemetryNoDescriptor
858 .
859 (constructor
860 NativeTelemetrySinkDecision
861 NativeTelemetrySinkRejected
862 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
863 state))
864 (branch
865 NativeTelemetrySomeDescriptor
866 descriptor
867 .
868 (eliminate
869 NativeTelemetryEncodedRecord
870 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
871 (family NativeTelemetrySinkDecision))
872 record
873 (branch
874 NativeTelemetryEncodedRecordValue
875 bytes
876 extent
877 digest
878 identity
879 .
880 (nat-eliminate
881 (lambda unrestricted exact : Nat . (family NativeTelemetrySinkDecision))
882 (constructor
883 NativeTelemetrySinkDecision
884 NativeTelemetrySinkRejected
885 (constructor NativeTelemetryErrorCode NativeTelemetryWriteShort)
886 state)
887 (lambda unrestricted exactPredecessor : Nat .
888 (lambda unrestricted ignoredExact : (family NativeTelemetrySinkDecision) .
889 (eliminate
890 NativeTelemetrySinkTelemetry
891 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
892 (family NativeTelemetrySinkDecision))
893 telemetry
894 (branch
895 NativeTelemetrySinkTelemetryValue
896 planned
897 completed
898 plannedBytes
899 oldWritten
900 syncs
901 closes
902 failures
903 fallbacks
904 .
905 (constructor
906 NativeTelemetrySinkDecision
907 NativeTelemetrySinkContinue
908 (constructor
909 NativeTelemetrySinkState
910 NativeTelemetrySinkStateValue
911 path
912 record
913 (constructor
914 NativeTelemetrySinkPhase
915 NativeTelemetrySinkSyncing)
916 optionalDescriptor
917 (constructor
918 NativeTelemetrySinkTelemetry
919 NativeTelemetrySinkTelemetryValue
920 (succ planned)
921 (succ completed)
922 plannedBytes
923 written
924 syncs
925 closes
926 failures
927 fallbacks))
928 (constructor
929 NativeTelemetrySinkAction
930 NativeTelemetrySinkIssueSyscall
931 (constructor LinuxSyscallRequest LinuxFdatasync descriptor)))))))
932 (modelWord64Equal written extent)))))))))
933 (branch
934 LinuxIoctlSucceeded
935 output
936 .
937 (constructor
938 NativeTelemetrySinkDecision
939 NativeTelemetrySinkRejected
940 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
941 state))
942 (branch
943 LinuxMmapSucceeded
944 address
945 .
946 (constructor
947 NativeTelemetrySinkDecision
948 NativeTelemetrySinkRejected
949 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
950 state))
951 (branch
952 LinuxUnitSucceeded
953 .
954 (constructor
955 NativeTelemetrySinkDecision
956 NativeTelemetrySinkRejected
957 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
958 state))
959 (branch
960 LinuxSyscallFailed
961 error
962 errno
963 .
964 (constructor
965 NativeTelemetrySinkDecision
966 NativeTelemetrySinkRejected
967 (constructor NativeTelemetryErrorCode NativeTelemetryWriteFailed)
968 state)))))
969
970def nativeTelemetrySinkAfterSync =
971 (lambda unrestricted response : (family LinuxSyscallResponse) .
972 (lambda unrestricted state : (family NativeTelemetrySinkState) .
973 (eliminate
974 LinuxSyscallResponse
975 (lambda unrestricted current : (family LinuxSyscallResponse) .
976 (family NativeTelemetrySinkDecision))
977 response
978 (branch
979 LinuxOpenSucceeded
980 descriptor
981 .
982 (constructor
983 NativeTelemetrySinkDecision
984 NativeTelemetrySinkRejected
985 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
986 state))
987 (branch
988 LinuxReadSucceeded
989 bytes
990 .
991 (constructor
992 NativeTelemetrySinkDecision
993 NativeTelemetrySinkRejected
994 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
995 state))
996 (branch
997 LinuxSeekSucceeded
998 position
999 .
1000 (constructor
1001 NativeTelemetrySinkDecision
1002 NativeTelemetrySinkRejected
1003 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1004 state))
1005 (branch
1006 LinuxWriteSucceeded
1007 written
1008 .
1009 (constructor
1010 NativeTelemetrySinkDecision
1011 NativeTelemetrySinkRejected
1012 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1013 state))
1014 (branch
1015 LinuxIoctlSucceeded
1016 output
1017 .
1018 (constructor
1019 NativeTelemetrySinkDecision
1020 NativeTelemetrySinkRejected
1021 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1022 state))
1023 (branch
1024 LinuxMmapSucceeded
1025 address
1026 .
1027 (constructor
1028 NativeTelemetrySinkDecision
1029 NativeTelemetrySinkRejected
1030 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1031 state))
1032 (branch
1033 LinuxUnitSucceeded
1034 .
1035 (eliminate
1036 NativeTelemetrySinkState
1037 (lambda unrestricted current : (family NativeTelemetrySinkState) .
1038 (family NativeTelemetrySinkDecision))
1039 state
1040 (branch
1041 NativeTelemetrySinkStateValue
1042 path
1043 record
1044 phase
1045 optionalDescriptor
1046 telemetry
1047 .
1048 (eliminate
1049 NativeTelemetryOptionalDescriptor
1050 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
1051 (family NativeTelemetrySinkDecision))
1052 optionalDescriptor
1053 (branch
1054 NativeTelemetryNoDescriptor
1055 .
1056 (constructor
1057 NativeTelemetrySinkDecision
1058 NativeTelemetrySinkRejected
1059 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1060 state))
1061 (branch
1062 NativeTelemetrySomeDescriptor
1063 descriptor
1064 .
1065 (eliminate
1066 NativeTelemetrySinkTelemetry
1067 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
1068 (family NativeTelemetrySinkDecision))
1069 telemetry
1070 (branch
1071 NativeTelemetrySinkTelemetryValue
1072 planned
1073 completed
1074 plannedBytes
1075 written
1076 syncs
1077 closes
1078 failures
1079 fallbacks
1080 .
1081 (constructor
1082 NativeTelemetrySinkDecision
1083 NativeTelemetrySinkContinue
1084 (constructor
1085 NativeTelemetrySinkState
1086 NativeTelemetrySinkStateValue
1087 path
1088 record
1089 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkClosing)
1090 optionalDescriptor
1091 (constructor
1092 NativeTelemetrySinkTelemetry
1093 NativeTelemetrySinkTelemetryValue
1094 (succ planned)
1095 (succ completed)
1096 plannedBytes
1097 written
1098 (succ syncs)
1099 closes
1100 failures
1101 fallbacks))
1102 (constructor
1103 NativeTelemetrySinkAction
1104 NativeTelemetrySinkIssueSyscall
1105 (constructor LinuxSyscallRequest LinuxClose descriptor))))))))))
1106 (branch
1107 LinuxSyscallFailed
1108 error
1109 errno
1110 .
1111 (constructor
1112 NativeTelemetrySinkDecision
1113 NativeTelemetrySinkRejected
1114 (constructor NativeTelemetryErrorCode NativeTelemetrySyncFailed)
1115 state)))))
1116
1117def nativeTelemetrySinkAfterClose =
1118 (lambda unrestricted response : (family LinuxSyscallResponse) .
1119 (lambda unrestricted state : (family NativeTelemetrySinkState) .
1120 (eliminate
1121 LinuxSyscallResponse
1122 (lambda unrestricted current : (family LinuxSyscallResponse) .
1123 (family NativeTelemetrySinkDecision))
1124 response
1125 (branch
1126 LinuxOpenSucceeded
1127 descriptor
1128 .
1129 (constructor
1130 NativeTelemetrySinkDecision
1131 NativeTelemetrySinkRejected
1132 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1133 state))
1134 (branch
1135 LinuxReadSucceeded
1136 bytes
1137 .
1138 (constructor
1139 NativeTelemetrySinkDecision
1140 NativeTelemetrySinkRejected
1141 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1142 state))
1143 (branch
1144 LinuxSeekSucceeded
1145 position
1146 .
1147 (constructor
1148 NativeTelemetrySinkDecision
1149 NativeTelemetrySinkRejected
1150 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1151 state))
1152 (branch
1153 LinuxWriteSucceeded
1154 written
1155 .
1156 (constructor
1157 NativeTelemetrySinkDecision
1158 NativeTelemetrySinkRejected
1159 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1160 state))
1161 (branch
1162 LinuxIoctlSucceeded
1163 output
1164 .
1165 (constructor
1166 NativeTelemetrySinkDecision
1167 NativeTelemetrySinkRejected
1168 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1169 state))
1170 (branch
1171 LinuxMmapSucceeded
1172 address
1173 .
1174 (constructor
1175 NativeTelemetrySinkDecision
1176 NativeTelemetrySinkRejected
1177 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1178 state))
1179 (branch
1180 LinuxUnitSucceeded
1181 .
1182 (eliminate
1183 NativeTelemetrySinkState
1184 (lambda unrestricted current : (family NativeTelemetrySinkState) .
1185 (family NativeTelemetrySinkDecision))
1186 state
1187 (branch
1188 NativeTelemetrySinkStateValue
1189 path
1190 record
1191 phase
1192 descriptor
1193 telemetry
1194 .
1195 (eliminate
1196 NativeTelemetrySinkTelemetry
1197 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
1198 (family NativeTelemetrySinkDecision))
1199 telemetry
1200 (branch
1201 NativeTelemetrySinkTelemetryValue
1202 planned
1203 completed
1204 plannedBytes
1205 written
1206 syncs
1207 closes
1208 failures
1209 fallbacks
1210 .
1211 (constructor
1212 NativeTelemetrySinkDecision
1213 NativeTelemetrySinkFinished
1214 record
1215 (constructor
1216 NativeTelemetrySinkTelemetry
1217 NativeTelemetrySinkTelemetryValue
1218 planned
1219 (succ completed)
1220 plannedBytes
1221 written
1222 syncs
1223 (succ closes)
1224 failures
1225 fallbacks)))))))
1226 (branch
1227 LinuxSyscallFailed
1228 error
1229 errno
1230 .
1231 (constructor
1232 NativeTelemetrySinkDecision
1233 NativeTelemetrySinkRejected
1234 (constructor NativeTelemetryErrorCode NativeTelemetryCloseFailed)
1235 state)))))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.