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)))))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.