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 nativeTelemetryRecordBody =
377 (lambda unrestricted sequence : (family ModelWord64) . (lambda unrestricted monotonic : (family ModelWord64) .
378 (lambda unrestricted domain : Byte . (lambda unrestricted event : Byte . (lambda unrestricted phase : Byte . (lambda unrestricted status : Byte .
379 (lambda unrestricted counters : (family NativeTelemetryCounters) . (lambda unrestricted identity : Bytes .
380 (lambda unrestricted errorCode : Bytes . (lambda unrestricted payload : Bytes .
381 (lambda unrestricted errorExtent : (family ModelWord64) . (lambda unrestricted payloadExtent : (family ModelWord64) .
382 (bytes-cons nativeTelemetryVersion (bytes-cons domain (bytes-cons event (bytes-cons phase (bytes-cons status
383 (nativeTelemetryBuildRecordPart1 sequence monotonic counters identity errorCode payload errorExtent payloadExtent))))))))))))))))))
384
385def nativeTelemetryBuildRecord =
386 (lambda unrestricted request : (family NativeTelemetryRecordRequest) .
387 (eliminate
388 NativeTelemetryRecordRequest
389 (lambda unrestricted current : (family NativeTelemetryRecordRequest) .
390 (family NativeTelemetryEncodeResult))
391 request
392 (branch
393 NativeTelemetryRecordRequestValue
394 sequence
395 monotonic
396 domain
397 event
398 phase
399 status
400 counters
401 identity
402 errorCode
403 payload
404 .
405 (nat-eliminate
406 (lambda unrestricted identityValid : Nat . (family NativeTelemetryEncodeResult))
407 (nativeTelemetryEncodeFailure
408 (constructor NativeTelemetryErrorCode NativeTelemetryIdentityInvalid)
409 (succ zero)
410 zero)
411 (lambda unrestricted identityPredecessor : Nat .
412 (lambda unrestricted ignoredIdentity : (family NativeTelemetryEncodeResult) .
413 (eliminate
414 NativeTelemetryCounterResult
415 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
416 (family NativeTelemetryEncodeResult))
417 (nativeTelemetryCounterFromNatural (bytes-length errorCode))
418 (branch
419 NativeTelemetryCounterSucceeded
420 errorExtent
421 .
422 (eliminate
423 NativeTelemetryCounterResult
424 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
425 (family NativeTelemetryEncodeResult))
426 (nativeTelemetryCounterFromNatural (bytes-length payload))
427 (branch
428 NativeTelemetryCounterSucceeded
429 payloadExtent
430 .
431 (app
432 (lambda unrestricted body : Bytes .
433 (app
434 (lambda unrestricted output : Bytes .
435 (eliminate
436 NativeTelemetryCounterResult
437 (lambda unrestricted current : (family NativeTelemetryCounterResult) .
438 (family NativeTelemetryEncodeResult))
439 (nativeTelemetryCounterFromNatural (bytes-length output))
440 (branch
441 NativeTelemetryCounterSucceeded
442 outputExtent
443 .
444 (constructor
445 NativeTelemetryEncodeResult
446 NativeTelemetryEncodeSucceeded
447 (constructor
448 NativeTelemetryEncodedRecord
449 NativeTelemetryEncodedRecordValue
450 output
451 outputExtent
452 (sha256HexBytesOrEmpty (sha256Hex body))
453 identity)
454 (nativeTelemetryEncodeTelemetry
455 (succ zero)
456 (bytes-length body)
457 (bytes-length output)
458 zero
459 zero
460 zero)))
461 (branch
462 NativeTelemetryCounterFailed
463 conversionError
464 naturalValue
465 .
466 (nativeTelemetryEncodeFailure
467 (constructor
468 NativeTelemetryErrorCode
469 NativeTelemetryPayloadLengthOverflow)
470 zero
471 (succ zero)))))
472 (bytes-append
473 nativeTelemetryMagic
474 (bytes-append body (sha256HexBytesOrEmpty (sha256Hex body))))))
475 (nativeTelemetryRecordBody
476 sequence monotonic domain event phase status counters identity errorCode payload errorExtent payloadExtent)))
477 (branch
478 NativeTelemetryCounterFailed
479 conversionError
480 naturalValue
481 .
482 (nativeTelemetryEncodeFailure
483 (constructor NativeTelemetryErrorCode NativeTelemetryPayloadLengthOverflow)
484 zero
485 (succ zero)))))
486 (branch
487 NativeTelemetryCounterFailed
488 conversionError
489 naturalValue
490 .
491 (nativeTelemetryEncodeFailure
492 (constructor NativeTelemetryErrorCode NativeTelemetryErrorLengthOverflow)
493 zero
494 (succ zero))))))
495 (naturalEqual (bytes-length identity) nativeTelemetryDigestBytes)))))
496
497def nativeTelemetryAppendFlags : (family ModelWord64) =
498 525377
499
500def nativeTelemetryOwnerReadWriteMode : (family ModelWord64) =
501 384
502
503def nativeTelemetrySinkTelemetryInitial =
504 (lambda unrestricted extent : (family ModelWord64) .
505 (constructor
506 NativeTelemetrySinkTelemetry
507 NativeTelemetrySinkTelemetryValue
508 (succ zero)
509 zero
510 extent
511 nativeTelemetryZeroWord64
512 zero
513 zero
514 zero
515 zero))
516
517def nativeTelemetryOpenAppendRequest =
518 (lambda unrestricted path : Bytes .
519 (constructor
520 LinuxSyscallRequest
521 LinuxOpenAt
522 linuxAtFdcwd
523 path
524 nativeTelemetryAppendFlags
525 nativeTelemetryOwnerReadWriteMode))
526
527def nativeTelemetrySinkBegin =
528 (lambda unrestricted path : Bytes .
529 (lambda unrestricted record : (family NativeTelemetryEncodedRecord) .
530 (eliminate
531 NativeTelemetryEncodedRecord
532 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
533 (family NativeTelemetrySinkDecision))
534 record
535 (branch
536 NativeTelemetryEncodedRecordValue
537 bytes
538 extent
539 digest
540 identity
541 .
542 (app
543 (lambda unrestricted initialState : (family NativeTelemetrySinkState) .
544 (nat-eliminate
545 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
546 (constructor
547 NativeTelemetrySinkDecision
548 NativeTelemetrySinkRejected
549 (constructor NativeTelemetryErrorCode NativeTelemetryPathEmpty)
550 initialState)
551 (lambda unrestricted pathPredecessor : Nat .
552 (lambda unrestricted ignoredPath : (family NativeTelemetrySinkDecision) .
553 (nat-eliminate
554 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
555 (constructor
556 NativeTelemetrySinkDecision
557 NativeTelemetrySinkRejected
558 (constructor NativeTelemetryErrorCode NativeTelemetryRecordEmpty)
559 initialState)
560 (lambda unrestricted recordPredecessor : Nat .
561 (lambda unrestricted ignoredRecord : (family NativeTelemetrySinkDecision) .
562 (constructor
563 NativeTelemetrySinkDecision
564 NativeTelemetrySinkContinue
565 initialState
566 (constructor
567 NativeTelemetrySinkAction
568 NativeTelemetrySinkIssueSyscall
569 (nativeTelemetryOpenAppendRequest path)))))
570 (bytes-length bytes))))
571 (bytes-length path)))
572 (constructor
573 NativeTelemetrySinkState
574 NativeTelemetrySinkStateValue
575 path
576 record
577 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkOpening)
578 (constructor NativeTelemetryOptionalDescriptor NativeTelemetryNoDescriptor)
579 (nativeTelemetrySinkTelemetryInitial extent)))))))
580
581def nativeTelemetrySinkAfterOpen =
582 (lambda unrestricted response : (family LinuxSyscallResponse) .
583 (lambda unrestricted state : (family NativeTelemetrySinkState) .
584 (eliminate
585 LinuxSyscallResponse
586 (lambda unrestricted current : (family LinuxSyscallResponse) .
587 (family NativeTelemetrySinkDecision))
588 response
589 (branch
590 LinuxOpenSucceeded
591 descriptor
592 .
593 (eliminate
594 NativeTelemetrySinkState
595 (lambda unrestricted current : (family NativeTelemetrySinkState) .
596 (family NativeTelemetrySinkDecision))
597 state
598 (branch
599 NativeTelemetrySinkStateValue
600 path
601 record
602 phase
603 oldDescriptor
604 telemetry
605 .
606 (eliminate
607 NativeTelemetryEncodedRecord
608 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
609 (family NativeTelemetrySinkDecision))
610 record
611 (branch
612 NativeTelemetryEncodedRecordValue
613 bytes
614 extent
615 digest
616 identity
617 .
618 (eliminate
619 NativeTelemetrySinkTelemetry
620 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
621 (family NativeTelemetrySinkDecision))
622 telemetry
623 (branch
624 NativeTelemetrySinkTelemetryValue
625 planned
626 completed
627 plannedBytes
628 written
629 syncs
630 closes
631 failures
632 fallbacks
633 .
634 (constructor
635 NativeTelemetrySinkDecision
636 NativeTelemetrySinkContinue
637 (constructor
638 NativeTelemetrySinkState
639 NativeTelemetrySinkStateValue
640 path
641 record
642 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkWriting)
643 (constructor
644 NativeTelemetryOptionalDescriptor
645 NativeTelemetrySomeDescriptor
646 descriptor)
647 (constructor
648 NativeTelemetrySinkTelemetry
649 NativeTelemetrySinkTelemetryValue
650 (succ planned)
651 (succ completed)
652 plannedBytes
653 written
654 syncs
655 closes
656 failures
657 fallbacks))
658 (constructor
659 NativeTelemetrySinkAction
660 NativeTelemetrySinkIssueSyscall
661 (constructor LinuxSyscallRequest LinuxWrite descriptor bytes))))))))))
662 (branch
663 LinuxReadSucceeded
664 bytes
665 .
666 (constructor
667 NativeTelemetrySinkDecision
668 NativeTelemetrySinkRejected
669 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
670 state))
671 (branch
672 LinuxSeekSucceeded
673 position
674 .
675 (constructor
676 NativeTelemetrySinkDecision
677 NativeTelemetrySinkRejected
678 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
679 state))
680 (branch
681 LinuxWriteSucceeded
682 written
683 .
684 (constructor
685 NativeTelemetrySinkDecision
686 NativeTelemetrySinkRejected
687 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
688 state))
689 (branch
690 LinuxIoctlSucceeded
691 output
692 .
693 (constructor
694 NativeTelemetrySinkDecision
695 NativeTelemetrySinkRejected
696 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
697 state))
698 (branch
699 LinuxMmapSucceeded
700 address
701 .
702 (constructor
703 NativeTelemetrySinkDecision
704 NativeTelemetrySinkRejected
705 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
706 state))
707 (branch
708 LinuxUnitSucceeded
709 .
710 (constructor
711 NativeTelemetrySinkDecision
712 NativeTelemetrySinkRejected
713 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
714 state))
715 (branch
716 LinuxSyscallFailed
717 error
718 errno
719 .
720 (constructor
721 NativeTelemetrySinkDecision
722 NativeTelemetrySinkRejected
723 (constructor NativeTelemetryErrorCode NativeTelemetryOpenFailed)
724 state)))))
725
726def nativeTelemetrySinkAfterWrite =
727 (lambda unrestricted response : (family LinuxSyscallResponse) .
728 (lambda unrestricted state : (family NativeTelemetrySinkState) .
729 (eliminate
730 LinuxSyscallResponse
731 (lambda unrestricted current : (family LinuxSyscallResponse) .
732 (family NativeTelemetrySinkDecision))
733 response
734 (branch
735 LinuxOpenSucceeded
736 descriptor
737 .
738 (constructor
739 NativeTelemetrySinkDecision
740 NativeTelemetrySinkRejected
741 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
742 state))
743 (branch
744 LinuxReadSucceeded
745 bytes
746 .
747 (constructor
748 NativeTelemetrySinkDecision
749 NativeTelemetrySinkRejected
750 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
751 state))
752 (branch
753 LinuxSeekSucceeded
754 position
755 .
756 (constructor
757 NativeTelemetrySinkDecision
758 NativeTelemetrySinkRejected
759 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
760 state))
761 (branch
762 LinuxWriteSucceeded
763 written
764 .
765 (eliminate
766 NativeTelemetrySinkState
767 (lambda unrestricted current : (family NativeTelemetrySinkState) .
768 (family NativeTelemetrySinkDecision))
769 state
770 (branch
771 NativeTelemetrySinkStateValue
772 path
773 record
774 phase
775 optionalDescriptor
776 telemetry
777 .
778 (eliminate
779 NativeTelemetryOptionalDescriptor
780 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
781 (family NativeTelemetrySinkDecision))
782 optionalDescriptor
783 (branch
784 NativeTelemetryNoDescriptor
785 .
786 (constructor
787 NativeTelemetrySinkDecision
788 NativeTelemetrySinkRejected
789 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
790 state))
791 (branch
792 NativeTelemetrySomeDescriptor
793 descriptor
794 .
795 (eliminate
796 NativeTelemetryEncodedRecord
797 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
798 (family NativeTelemetrySinkDecision))
799 record
800 (branch
801 NativeTelemetryEncodedRecordValue
802 bytes
803 extent
804 digest
805 identity
806 .
807 (nat-eliminate
808 (lambda unrestricted exact : Nat . (family NativeTelemetrySinkDecision))
809 (constructor
810 NativeTelemetrySinkDecision
811 NativeTelemetrySinkRejected
812 (constructor NativeTelemetryErrorCode NativeTelemetryWriteShort)
813 state)
814 (lambda unrestricted exactPredecessor : Nat .
815 (lambda unrestricted ignoredExact : (family NativeTelemetrySinkDecision) .
816 (eliminate
817 NativeTelemetrySinkTelemetry
818 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
819 (family NativeTelemetrySinkDecision))
820 telemetry
821 (branch
822 NativeTelemetrySinkTelemetryValue
823 planned
824 completed
825 plannedBytes
826 oldWritten
827 syncs
828 closes
829 failures
830 fallbacks
831 .
832 (constructor
833 NativeTelemetrySinkDecision
834 NativeTelemetrySinkContinue
835 (constructor
836 NativeTelemetrySinkState
837 NativeTelemetrySinkStateValue
838 path
839 record
840 (constructor
841 NativeTelemetrySinkPhase
842 NativeTelemetrySinkSyncing)
843 optionalDescriptor
844 (constructor
845 NativeTelemetrySinkTelemetry
846 NativeTelemetrySinkTelemetryValue
847 (succ planned)
848 (succ completed)
849 plannedBytes
850 written
851 syncs
852 closes
853 failures
854 fallbacks))
855 (constructor
856 NativeTelemetrySinkAction
857 NativeTelemetrySinkIssueSyscall
858 (constructor LinuxSyscallRequest LinuxFdatasync descriptor)))))))
859 (modelWord64Equal written extent)))))))))
860 (branch
861 LinuxIoctlSucceeded
862 output
863 .
864 (constructor
865 NativeTelemetrySinkDecision
866 NativeTelemetrySinkRejected
867 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
868 state))
869 (branch
870 LinuxMmapSucceeded
871 address
872 .
873 (constructor
874 NativeTelemetrySinkDecision
875 NativeTelemetrySinkRejected
876 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
877 state))
878 (branch
879 LinuxUnitSucceeded
880 .
881 (constructor
882 NativeTelemetrySinkDecision
883 NativeTelemetrySinkRejected
884 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
885 state))
886 (branch
887 LinuxSyscallFailed
888 error
889 errno
890 .
891 (constructor
892 NativeTelemetrySinkDecision
893 NativeTelemetrySinkRejected
894 (constructor NativeTelemetryErrorCode NativeTelemetryWriteFailed)
895 state)))))
896
897def nativeTelemetrySinkAfterSync =
898 (lambda unrestricted response : (family LinuxSyscallResponse) .
899 (lambda unrestricted state : (family NativeTelemetrySinkState) .
900 (eliminate
901 LinuxSyscallResponse
902 (lambda unrestricted current : (family LinuxSyscallResponse) .
903 (family NativeTelemetrySinkDecision))
904 response
905 (branch
906 LinuxOpenSucceeded
907 descriptor
908 .
909 (constructor
910 NativeTelemetrySinkDecision
911 NativeTelemetrySinkRejected
912 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
913 state))
914 (branch
915 LinuxReadSucceeded
916 bytes
917 .
918 (constructor
919 NativeTelemetrySinkDecision
920 NativeTelemetrySinkRejected
921 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
922 state))
923 (branch
924 LinuxSeekSucceeded
925 position
926 .
927 (constructor
928 NativeTelemetrySinkDecision
929 NativeTelemetrySinkRejected
930 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
931 state))
932 (branch
933 LinuxWriteSucceeded
934 written
935 .
936 (constructor
937 NativeTelemetrySinkDecision
938 NativeTelemetrySinkRejected
939 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
940 state))
941 (branch
942 LinuxIoctlSucceeded
943 output
944 .
945 (constructor
946 NativeTelemetrySinkDecision
947 NativeTelemetrySinkRejected
948 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
949 state))
950 (branch
951 LinuxMmapSucceeded
952 address
953 .
954 (constructor
955 NativeTelemetrySinkDecision
956 NativeTelemetrySinkRejected
957 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
958 state))
959 (branch
960 LinuxUnitSucceeded
961 .
962 (eliminate
963 NativeTelemetrySinkState
964 (lambda unrestricted current : (family NativeTelemetrySinkState) .
965 (family NativeTelemetrySinkDecision))
966 state
967 (branch
968 NativeTelemetrySinkStateValue
969 path
970 record
971 phase
972 optionalDescriptor
973 telemetry
974 .
975 (eliminate
976 NativeTelemetryOptionalDescriptor
977 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
978 (family NativeTelemetrySinkDecision))
979 optionalDescriptor
980 (branch
981 NativeTelemetryNoDescriptor
982 .
983 (constructor
984 NativeTelemetrySinkDecision
985 NativeTelemetrySinkRejected
986 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
987 state))
988 (branch
989 NativeTelemetrySomeDescriptor
990 descriptor
991 .
992 (eliminate
993 NativeTelemetrySinkTelemetry
994 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
995 (family NativeTelemetrySinkDecision))
996 telemetry
997 (branch
998 NativeTelemetrySinkTelemetryValue
999 planned
1000 completed
1001 plannedBytes
1002 written
1003 syncs
1004 closes
1005 failures
1006 fallbacks
1007 .
1008 (constructor
1009 NativeTelemetrySinkDecision
1010 NativeTelemetrySinkContinue
1011 (constructor
1012 NativeTelemetrySinkState
1013 NativeTelemetrySinkStateValue
1014 path
1015 record
1016 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkClosing)
1017 optionalDescriptor
1018 (constructor
1019 NativeTelemetrySinkTelemetry
1020 NativeTelemetrySinkTelemetryValue
1021 (succ planned)
1022 (succ completed)
1023 plannedBytes
1024 written
1025 (succ syncs)
1026 closes
1027 failures
1028 fallbacks))
1029 (constructor
1030 NativeTelemetrySinkAction
1031 NativeTelemetrySinkIssueSyscall
1032 (constructor LinuxSyscallRequest LinuxClose descriptor))))))))))
1033 (branch
1034 LinuxSyscallFailed
1035 error
1036 errno
1037 .
1038 (constructor
1039 NativeTelemetrySinkDecision
1040 NativeTelemetrySinkRejected
1041 (constructor NativeTelemetryErrorCode NativeTelemetrySyncFailed)
1042 state)))))
1043
1044def nativeTelemetrySinkAfterClose =
1045 (lambda unrestricted response : (family LinuxSyscallResponse) .
1046 (lambda unrestricted state : (family NativeTelemetrySinkState) .
1047 (eliminate
1048 LinuxSyscallResponse
1049 (lambda unrestricted current : (family LinuxSyscallResponse) .
1050 (family NativeTelemetrySinkDecision))
1051 response
1052 (branch
1053 LinuxOpenSucceeded
1054 descriptor
1055 .
1056 (constructor
1057 NativeTelemetrySinkDecision
1058 NativeTelemetrySinkRejected
1059 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1060 state))
1061 (branch
1062 LinuxReadSucceeded
1063 bytes
1064 .
1065 (constructor
1066 NativeTelemetrySinkDecision
1067 NativeTelemetrySinkRejected
1068 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1069 state))
1070 (branch
1071 LinuxSeekSucceeded
1072 position
1073 .
1074 (constructor
1075 NativeTelemetrySinkDecision
1076 NativeTelemetrySinkRejected
1077 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1078 state))
1079 (branch
1080 LinuxWriteSucceeded
1081 written
1082 .
1083 (constructor
1084 NativeTelemetrySinkDecision
1085 NativeTelemetrySinkRejected
1086 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1087 state))
1088 (branch
1089 LinuxIoctlSucceeded
1090 output
1091 .
1092 (constructor
1093 NativeTelemetrySinkDecision
1094 NativeTelemetrySinkRejected
1095 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1096 state))
1097 (branch
1098 LinuxMmapSucceeded
1099 address
1100 .
1101 (constructor
1102 NativeTelemetrySinkDecision
1103 NativeTelemetrySinkRejected
1104 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
1105 state))
1106 (branch
1107 LinuxUnitSucceeded
1108 .
1109 (eliminate
1110 NativeTelemetrySinkState
1111 (lambda unrestricted current : (family NativeTelemetrySinkState) .
1112 (family NativeTelemetrySinkDecision))
1113 state
1114 (branch
1115 NativeTelemetrySinkStateValue
1116 path
1117 record
1118 phase
1119 descriptor
1120 telemetry
1121 .
1122 (eliminate
1123 NativeTelemetrySinkTelemetry
1124 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
1125 (family NativeTelemetrySinkDecision))
1126 telemetry
1127 (branch
1128 NativeTelemetrySinkTelemetryValue
1129 planned
1130 completed
1131 plannedBytes
1132 written
1133 syncs
1134 closes
1135 failures
1136 fallbacks
1137 .
1138 (constructor
1139 NativeTelemetrySinkDecision
1140 NativeTelemetrySinkFinished
1141 record
1142 (constructor
1143 NativeTelemetrySinkTelemetry
1144 NativeTelemetrySinkTelemetryValue
1145 planned
1146 (succ completed)
1147 plannedBytes
1148 written
1149 syncs
1150 (succ closes)
1151 failures
1152 fallbacks)))))))
1153 (branch
1154 LinuxSyscallFailed
1155 error
1156 errno
1157 .
1158 (constructor
1159 NativeTelemetrySinkDecision
1160 NativeTelemetrySinkRejected
1161 (constructor NativeTelemetryErrorCode NativeTelemetryCloseFailed)
1162 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.