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