module Runtime.NativeTelemetry

import Data.SHA256Digest
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Runtime.LinuxSyscall
import Std.Natural

family NativeTelemetryErrorCode : Type 0
constructor NativeTelemetryIdentityInvalid
constructor NativeTelemetryCounterOverflow
constructor NativeTelemetryErrorLengthOverflow
constructor NativeTelemetryPayloadLengthOverflow
constructor NativeTelemetryPathEmpty
constructor NativeTelemetryRecordEmpty
constructor NativeTelemetryOpenFailed
constructor NativeTelemetryWriteFailed
constructor NativeTelemetryWriteShort
constructor NativeTelemetrySyncFailed
constructor NativeTelemetryCloseFailed
constructor NativeTelemetryUnexpectedResponse
constructor NativeTelemetryTerminalStateReused
constructor NativeTelemetryHostFallbackObserved

end-family

family NativeTelemetryCounterResult : Type 0
constructor NativeTelemetryCounterSucceeded
field unrestricted nativeTelemetryCounterValue : (family ModelWord64)
constructor NativeTelemetryCounterFailed
field unrestricted nativeTelemetryCounterError : (family NativeTelemetryErrorCode)
field unrestricted nativeTelemetryCounterNatural : Nat

end-family

family NativeTelemetryCounters : Type 0
constructor NativeTelemetryCountersValue
field unrestricted nativeTelemetryCounter0 : (family ModelWord64)
field unrestricted nativeTelemetryCounter1 : (family ModelWord64)
field unrestricted nativeTelemetryCounter2 : (family ModelWord64)
field unrestricted nativeTelemetryCounter3 : (family ModelWord64)
field unrestricted nativeTelemetryCounter4 : (family ModelWord64)
field unrestricted nativeTelemetryCounter5 : (family ModelWord64)
field unrestricted nativeTelemetryCounter6 : (family ModelWord64)
field unrestricted nativeTelemetryCounter7 : (family ModelWord64)

end-family

family NativeTelemetryRecordRequest : Type 0
constructor NativeTelemetryRecordRequestValue
field unrestricted nativeTelemetryRequestSequence : (family ModelWord64)
field unrestricted nativeTelemetryRequestMonotonicNanoseconds : (family ModelWord64)
field unrestricted nativeTelemetryRequestDomain : Byte
field unrestricted nativeTelemetryRequestEvent : Byte
field unrestricted nativeTelemetryRequestPhase : Byte
field unrestricted nativeTelemetryRequestStatus : Byte
field unrestricted nativeTelemetryRequestCounters : (family NativeTelemetryCounters)
field unrestricted nativeTelemetryRequestIdentity : Bytes
field unrestricted nativeTelemetryRequestErrorCode : Bytes
field unrestricted nativeTelemetryRequestPayload : Bytes

end-family

family NativeTelemetryEncodeTelemetry : Type 0
constructor NativeTelemetryEncodeTelemetryValue
field unrestricted nativeTelemetryEncodedRecords : Nat
field unrestricted nativeTelemetryEncodedBodyBytes : Nat
field unrestricted nativeTelemetryEncodedOutputBytes : Nat
field unrestricted nativeTelemetryIdentityRejections : Nat
field unrestricted nativeTelemetryLengthRejections : Nat
field unrestricted nativeTelemetryEncodingFailures : Nat
field unrestricted nativeTelemetryEncodingHostFallbacks : Nat

end-family

family NativeTelemetryEncodedRecord : Type 0
constructor NativeTelemetryEncodedRecordValue
field unrestricted nativeTelemetryEncodedBytes : Bytes
field unrestricted nativeTelemetryEncodedExtent : (family ModelWord64)
field unrestricted nativeTelemetryEncodedSHA256 : Bytes
field unrestricted nativeTelemetryEncodedIdentity : Bytes

end-family

family NativeTelemetryEncodeResult : Type 0
constructor NativeTelemetryEncodeSucceeded
field unrestricted nativeTelemetryEncodeRecord : (family NativeTelemetryEncodedRecord)
field unrestricted nativeTelemetryEncodeSuccessTelemetry : (family NativeTelemetryEncodeTelemetry)
constructor NativeTelemetryEncodeFailed
field unrestricted nativeTelemetryEncodeError : (family NativeTelemetryErrorCode)
field unrestricted nativeTelemetryEncodeFailureTelemetry : (family NativeTelemetryEncodeTelemetry)

end-family

family NativeTelemetrySinkPhase : Type 0
constructor NativeTelemetrySinkOpening
constructor NativeTelemetrySinkWriting
constructor NativeTelemetrySinkSyncing
constructor NativeTelemetrySinkClosing
constructor NativeTelemetrySinkComplete
constructor NativeTelemetrySinkFailed

end-family

family NativeTelemetryOptionalDescriptor : Type 0
constructor NativeTelemetryNoDescriptor
constructor NativeTelemetrySomeDescriptor
field unrestricted nativeTelemetrySomeDescriptorValue : (family LinuxFileDescriptor)

end-family

family NativeTelemetrySinkTelemetry : Type 0
constructor NativeTelemetrySinkTelemetryValue
field unrestricted nativeTelemetrySinkSyscallsPlanned : Nat
field unrestricted nativeTelemetrySinkSyscallsCompleted : Nat
field unrestricted nativeTelemetrySinkBytesPlanned : (family ModelWord64)
field unrestricted nativeTelemetrySinkBytesWritten : (family ModelWord64)
field unrestricted nativeTelemetrySinkSyncs : Nat
field unrestricted nativeTelemetrySinkCloses : Nat
field unrestricted nativeTelemetrySinkFailures : Nat
field unrestricted nativeTelemetrySinkHostFallbacks : Nat

end-family

family NativeTelemetrySinkState : Type 0
constructor NativeTelemetrySinkStateValue
field unrestricted nativeTelemetrySinkPath : Bytes
field unrestricted nativeTelemetrySinkRecord : (family NativeTelemetryEncodedRecord)
field unrestricted nativeTelemetrySinkPhaseValue : (family NativeTelemetrySinkPhase)
field unrestricted nativeTelemetrySinkDescriptor : (family NativeTelemetryOptionalDescriptor)
field unrestricted nativeTelemetrySinkTelemetryValue : (family NativeTelemetrySinkTelemetry)

end-family

family NativeTelemetrySinkAction : Type 0
constructor NativeTelemetrySinkIssueSyscall
field unrestricted nativeTelemetrySinkSyscallRequest : (family LinuxSyscallRequest)

end-family

family NativeTelemetrySinkDecision : Type 0
constructor NativeTelemetrySinkContinue
field unrestricted nativeTelemetrySinkContinueState : (family NativeTelemetrySinkState)
field unrestricted nativeTelemetrySinkContinueAction : (family NativeTelemetrySinkAction)
constructor NativeTelemetrySinkFinished
field unrestricted nativeTelemetrySinkFinishedRecord : (family NativeTelemetryEncodedRecord)
field unrestricted nativeTelemetrySinkFinishedTelemetry : (family NativeTelemetrySinkTelemetry)
constructor NativeTelemetrySinkRejected
field unrestricted nativeTelemetrySinkRejectedCode : (family NativeTelemetryErrorCode)
field unrestricted nativeTelemetrySinkRejectedState : (family NativeTelemetrySinkState)

end-family

def nativeTelemetryErrorCodeBytes =
  (lambda unrestricted code : (family NativeTelemetryErrorCode) .
    (eliminate
      NativeTelemetryErrorCode
      (lambda unrestricted current : (family NativeTelemetryErrorCode) . Bytes)
      code
      (branch NativeTelemetryIdentityInvalid . b"ALPHA-TEL-001")
      (branch NativeTelemetryCounterOverflow . b"ALPHA-TEL-002")
      (branch NativeTelemetryErrorLengthOverflow . b"ALPHA-TEL-003")
      (branch NativeTelemetryPayloadLengthOverflow . b"ALPHA-TEL-004")
      (branch NativeTelemetryPathEmpty . b"ALPHA-TEL-005")
      (branch NativeTelemetryRecordEmpty . b"ALPHA-TEL-006")
      (branch NativeTelemetryOpenFailed . b"ALPHA-TEL-007")
      (branch NativeTelemetryWriteFailed . b"ALPHA-TEL-008")
      (branch NativeTelemetryWriteShort . b"ALPHA-TEL-009")
      (branch NativeTelemetrySyncFailed . b"ALPHA-TEL-010")
      (branch NativeTelemetryCloseFailed . b"ALPHA-TEL-011")
      (branch NativeTelemetryUnexpectedResponse . b"ALPHA-TEL-012")
      (branch NativeTelemetryTerminalStateReused . b"ALPHA-TEL-013")
      (branch NativeTelemetryHostFallbackObserved . b"ALPHA-TEL-014")))

def nativeTelemetryMagic : Bytes =
  b"ALPHATEL"

def nativeTelemetryVersion : Byte =
  (byte 1)

def nativeTelemetryDigestBytes : Nat =
  (byte-to-nat (byte 64))

def nativeTelemetryZeroWord64 : (family ModelWord64) =
  0

def nativeTelemetryWord32ToWord64 =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . (family ModelWord64))
      value
      (branch
        ModelWord32Value
        byte0
        byte1
        byte2
        byte3
        .
        (constructor
          ModelWord64
          ModelWord64Value
          byte0
          byte1
          byte2
          byte3
          (byte 0)
          (byte 0)
          (byte 0)
          (byte 0)))))

def nativeTelemetryWord32Bytes =
  (lambda unrestricted value : (family ModelWord32) .
    (eliminate
      ModelWord32
      (lambda unrestricted current : (family ModelWord32) . Bytes)
      value
      (branch
        ModelWord32Value
        byte0
        byte1
        byte2
        byte3
        .
        (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))

def nativeTelemetryWord64Bytes =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate
      ModelWord64
      (lambda unrestricted current : (family ModelWord64) . Bytes)
      value
      (branch
        ModelWord64Value
        byte0
        byte1
        byte2
        byte3
        byte4
        byte5
        byte6
        byte7
        .
        (bytes-cons
          byte0
          (bytes-cons
            byte1
            (bytes-cons
              byte2
              (bytes-cons
                byte3
                (bytes-cons byte4 (bytes-cons byte5 (bytes-cons byte6 (bytes-cons byte7 b"")))))))))))

def nativeTelemetryCounterFromNatural =
  (lambda unrestricted value : Nat .
    (app
      (lambda unrestricted encoded : (family ModelWord32) .
        (nat-eliminate
          (lambda unrestricted exact : Nat . (family NativeTelemetryCounterResult))
          (constructor
            NativeTelemetryCounterResult
            NativeTelemetryCounterFailed
            (constructor NativeTelemetryErrorCode NativeTelemetryCounterOverflow)
            value)
          (lambda unrestricted exactPredecessor : Nat .
            (lambda unrestricted ignoredExact : (family NativeTelemetryCounterResult) .
              (constructor
                NativeTelemetryCounterResult
                NativeTelemetryCounterSucceeded
                (nativeTelemetryWord32ToWord64 encoded))))
          (naturalEqual (modelWord32ToNatural encoded) value)))
      (modelWord32FromNaturalTruncated value)))

def nativeTelemetryEncodeTelemetry =
  (lambda unrestricted records : Nat .
    (lambda unrestricted bodyBytes : Nat .
      (lambda unrestricted outputBytes : Nat .
        (lambda unrestricted identityRejections : Nat .
          (lambda unrestricted lengthRejections : Nat .
            (lambda unrestricted failures : Nat .
              (constructor
                NativeTelemetryEncodeTelemetry
                NativeTelemetryEncodeTelemetryValue
                records
                bodyBytes
                outputBytes
                identityRejections
                lengthRejections
                failures
                zero)))))))

def nativeTelemetryEncodeFailure =
  (lambda unrestricted code : (family NativeTelemetryErrorCode) .
    (lambda unrestricted identityRejections : Nat .
      (lambda unrestricted lengthRejections : Nat .
        (constructor
          NativeTelemetryEncodeResult
          NativeTelemetryEncodeFailed
          code
          (nativeTelemetryEncodeTelemetry
            zero
            zero
            zero
            identityRejections
            lengthRejections
            (succ zero))))))

def nativeTelemetryEncodeCounters =
  (lambda unrestricted counters : (family NativeTelemetryCounters) .
    (eliminate
      NativeTelemetryCounters
      (lambda unrestricted current : (family NativeTelemetryCounters) . Bytes)
      counters
      (branch
        NativeTelemetryCountersValue
        counter0
        counter1
        counter2
        counter3
        counter4
        counter5
        counter6
        counter7
        .
        (bytes-builder-build
          (bytes-builder-append
            (bytes-builder-chunk (nativeTelemetryWord64Bytes counter0))
            (bytes-builder-append
              (bytes-builder-chunk (nativeTelemetryWord64Bytes counter1))
              (bytes-builder-append
                (bytes-builder-chunk (nativeTelemetryWord64Bytes counter2))
                (bytes-builder-append
                  (bytes-builder-chunk (nativeTelemetryWord64Bytes counter3))
                  (bytes-builder-append
                    (bytes-builder-chunk (nativeTelemetryWord64Bytes counter4))
                    (bytes-builder-append
                      (bytes-builder-chunk (nativeTelemetryWord64Bytes counter5))
                      (bytes-builder-append
                        (bytes-builder-chunk (nativeTelemetryWord64Bytes counter6))
                        (bytes-builder-chunk (nativeTelemetryWord64Bytes counter7)))))))))))))

-- Part of `nativeTelemetryBuildRecord`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def nativeTelemetryBuildRecordPart1 =
  (lambda unrestricted sequence : (family ModelWord64) .
    (lambda unrestricted monotonic : (family ModelWord64) .
      (lambda unrestricted counters : (family NativeTelemetryCounters) .
        (lambda unrestricted identity : Bytes .
          (lambda unrestricted errorCode : Bytes .
            (lambda unrestricted payload : Bytes .
              (lambda unrestricted errorExtent : (family ModelWord64) .
                (lambda unrestricted payloadExtent : (family ModelWord64) .
                  (bytes-builder-build
                    (bytes-builder-append
                      (bytes-builder-chunk (nativeTelemetryWord64Bytes sequence))
                      (bytes-builder-append
                        (bytes-builder-chunk (nativeTelemetryWord64Bytes monotonic))
                        (bytes-builder-append
                          (bytes-builder-chunk (nativeTelemetryEncodeCounters counters))
                          (bytes-builder-append
                            (bytes-builder-chunk identity)
                            (bytes-builder-append
                              (bytes-builder-chunk (nativeTelemetryWord64Bytes errorExtent))
                              (bytes-builder-append
                                (bytes-builder-chunk errorCode)
                                (bytes-builder-append
                                  (bytes-builder-chunk (nativeTelemetryWord64Bytes payloadExtent))
                                  (bytes-builder-chunk payload)))))))))))))))))

-- The record's body -- what its digest covers -- from its fields and the
-- two extents; `nativeTelemetryBuildRecord` frames it with the magic and
-- the digest, and an executable that seals a record at run time
-- (Runtime.NativeTelemetrySeal) starts from it.
def nativeTelemetryRecordBody =
  (lambda unrestricted sequence : (family ModelWord64) . (lambda unrestricted monotonic : (family ModelWord64) .
  (lambda unrestricted domain : Byte . (lambda unrestricted event : Byte . (lambda unrestricted phase : Byte . (lambda unrestricted status : Byte .
  (lambda unrestricted counters : (family NativeTelemetryCounters) . (lambda unrestricted identity : Bytes .
  (lambda unrestricted errorCode : Bytes . (lambda unrestricted payload : Bytes .
  (lambda unrestricted errorExtent : (family ModelWord64) . (lambda unrestricted payloadExtent : (family ModelWord64) .
    (bytes-cons nativeTelemetryVersion (bytes-cons domain (bytes-cons event (bytes-cons phase (bytes-cons status
      (nativeTelemetryBuildRecordPart1 sequence monotonic counters identity errorCode payload errorExtent payloadExtent))))))))))))))))))

def nativeTelemetryBuildRecord =
  (lambda unrestricted request : (family NativeTelemetryRecordRequest) .
    (eliminate
      NativeTelemetryRecordRequest
      (lambda unrestricted current : (family NativeTelemetryRecordRequest) .
        (family NativeTelemetryEncodeResult))
      request
      (branch
        NativeTelemetryRecordRequestValue
        sequence
        monotonic
        domain
        event
        phase
        status
        counters
        identity
        errorCode
        payload
        .
        (nat-eliminate
          (lambda unrestricted identityValid : Nat . (family NativeTelemetryEncodeResult))
          (nativeTelemetryEncodeFailure
            (constructor NativeTelemetryErrorCode NativeTelemetryIdentityInvalid)
            (succ zero)
            zero)
          (lambda unrestricted identityPredecessor : Nat .
            (lambda unrestricted ignoredIdentity : (family NativeTelemetryEncodeResult) .
              (eliminate
                NativeTelemetryCounterResult
                (lambda unrestricted current : (family NativeTelemetryCounterResult) .
                  (family NativeTelemetryEncodeResult))
                (nativeTelemetryCounterFromNatural (bytes-length errorCode))
                (branch
                  NativeTelemetryCounterSucceeded
                  errorExtent
                  .
                  (eliminate
                    NativeTelemetryCounterResult
                    (lambda unrestricted current : (family NativeTelemetryCounterResult) .
                      (family NativeTelemetryEncodeResult))
                    (nativeTelemetryCounterFromNatural (bytes-length payload))
                    (branch
                      NativeTelemetryCounterSucceeded
                      payloadExtent
                      .
                      (app
                        (lambda unrestricted body : Bytes .
                          (app
                            (lambda unrestricted output : Bytes .
                              (eliminate
                                NativeTelemetryCounterResult
                                (lambda unrestricted current : (family NativeTelemetryCounterResult) .
                                  (family NativeTelemetryEncodeResult))
                                (nativeTelemetryCounterFromNatural (bytes-length output))
                                (branch
                                  NativeTelemetryCounterSucceeded
                                  outputExtent
                                  .
                                  (constructor
                                    NativeTelemetryEncodeResult
                                    NativeTelemetryEncodeSucceeded
                                    (constructor
                                      NativeTelemetryEncodedRecord
                                      NativeTelemetryEncodedRecordValue
                                      output
                                      outputExtent
                                      (sha256HexBytesOrEmpty (sha256Hex body))
                                      identity)
                                    (nativeTelemetryEncodeTelemetry
                                      (succ zero)
                                      (bytes-length body)
                                      (bytes-length output)
                                      zero
                                      zero
                                      zero)))
                                (branch
                                  NativeTelemetryCounterFailed
                                  conversionError
                                  naturalValue
                                  .
                                  (nativeTelemetryEncodeFailure
                                    (constructor
                                      NativeTelemetryErrorCode
                                      NativeTelemetryPayloadLengthOverflow)
                                    zero
                                    (succ zero)))))
                            (bytes-append
                              nativeTelemetryMagic
                              (bytes-append body (sha256HexBytesOrEmpty (sha256Hex body))))))
                        (nativeTelemetryRecordBody
                          sequence monotonic domain event phase status counters identity errorCode payload errorExtent payloadExtent)))
                    (branch
                      NativeTelemetryCounterFailed
                      conversionError
                      naturalValue
                      .
                      (nativeTelemetryEncodeFailure
                        (constructor NativeTelemetryErrorCode NativeTelemetryPayloadLengthOverflow)
                        zero
                        (succ zero)))))
                (branch
                  NativeTelemetryCounterFailed
                  conversionError
                  naturalValue
                  .
                  (nativeTelemetryEncodeFailure
                    (constructor NativeTelemetryErrorCode NativeTelemetryErrorLengthOverflow)
                    zero
                    (succ zero))))))
          (naturalEqual (bytes-length identity) nativeTelemetryDigestBytes)))))

def nativeTelemetryAppendFlags : (family ModelWord64) =
  525377

def nativeTelemetryOwnerReadWriteMode : (family ModelWord64) =
  384

def nativeTelemetrySinkTelemetryInitial =
  (lambda unrestricted extent : (family ModelWord64) .
    (constructor
      NativeTelemetrySinkTelemetry
      NativeTelemetrySinkTelemetryValue
      (succ zero)
      zero
      extent
      nativeTelemetryZeroWord64
      zero
      zero
      zero
      zero))

def nativeTelemetryOpenAppendRequest =
  (lambda unrestricted path : Bytes .
    (constructor
      LinuxSyscallRequest
      LinuxOpenAt
      linuxAtFdcwd
      path
      nativeTelemetryAppendFlags
      nativeTelemetryOwnerReadWriteMode))

def nativeTelemetrySinkBegin =
  (lambda unrestricted path : Bytes .
    (lambda unrestricted record : (family NativeTelemetryEncodedRecord) .
      (eliminate
        NativeTelemetryEncodedRecord
        (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
          (family NativeTelemetrySinkDecision))
        record
        (branch
          NativeTelemetryEncodedRecordValue
          bytes
          extent
          digest
          identity
          .
          (app
            (lambda unrestricted initialState : (family NativeTelemetrySinkState) .
              (nat-eliminate
                (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
                (constructor
                  NativeTelemetrySinkDecision
                  NativeTelemetrySinkRejected
                  (constructor NativeTelemetryErrorCode NativeTelemetryPathEmpty)
                  initialState)
                (lambda unrestricted pathPredecessor : Nat .
                  (lambda unrestricted ignoredPath : (family NativeTelemetrySinkDecision) .
                    (nat-eliminate
                      (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
                      (constructor
                        NativeTelemetrySinkDecision
                        NativeTelemetrySinkRejected
                        (constructor NativeTelemetryErrorCode NativeTelemetryRecordEmpty)
                        initialState)
                      (lambda unrestricted recordPredecessor : Nat .
                        (lambda unrestricted ignoredRecord : (family NativeTelemetrySinkDecision) .
                          (constructor
                            NativeTelemetrySinkDecision
                            NativeTelemetrySinkContinue
                            initialState
                            (constructor
                              NativeTelemetrySinkAction
                              NativeTelemetrySinkIssueSyscall
                              (nativeTelemetryOpenAppendRequest path)))))
                      (bytes-length bytes))))
                (bytes-length path)))
            (constructor
              NativeTelemetrySinkState
              NativeTelemetrySinkStateValue
              path
              record
              (constructor NativeTelemetrySinkPhase NativeTelemetrySinkOpening)
              (constructor NativeTelemetryOptionalDescriptor NativeTelemetryNoDescriptor)
              (nativeTelemetrySinkTelemetryInitial extent)))))))

def nativeTelemetrySinkAfterOpen =
  (lambda unrestricted response : (family LinuxSyscallResponse) .
    (lambda unrestricted state : (family NativeTelemetrySinkState) .
      (eliminate
        LinuxSyscallResponse
        (lambda unrestricted current : (family LinuxSyscallResponse) .
          (family NativeTelemetrySinkDecision))
        response
        (branch
          LinuxOpenSucceeded
          descriptor
          .
          (eliminate
            NativeTelemetrySinkState
            (lambda unrestricted current : (family NativeTelemetrySinkState) .
              (family NativeTelemetrySinkDecision))
            state
            (branch
              NativeTelemetrySinkStateValue
              path
              record
              phase
              oldDescriptor
              telemetry
              .
              (eliminate
                NativeTelemetryEncodedRecord
                (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
                  (family NativeTelemetrySinkDecision))
                record
                (branch
                  NativeTelemetryEncodedRecordValue
                  bytes
                  extent
                  digest
                  identity
                  .
                  (eliminate
                    NativeTelemetrySinkTelemetry
                    (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
                      (family NativeTelemetrySinkDecision))
                    telemetry
                    (branch
                      NativeTelemetrySinkTelemetryValue
                      planned
                      completed
                      plannedBytes
                      written
                      syncs
                      closes
                      failures
                      fallbacks
                      .
                      (constructor
                        NativeTelemetrySinkDecision
                        NativeTelemetrySinkContinue
                        (constructor
                          NativeTelemetrySinkState
                          NativeTelemetrySinkStateValue
                          path
                          record
                          (constructor NativeTelemetrySinkPhase NativeTelemetrySinkWriting)
                          (constructor
                            NativeTelemetryOptionalDescriptor
                            NativeTelemetrySomeDescriptor
                            descriptor)
                          (constructor
                            NativeTelemetrySinkTelemetry
                            NativeTelemetrySinkTelemetryValue
                            (succ planned)
                            (succ completed)
                            plannedBytes
                            written
                            syncs
                            closes
                            failures
                            fallbacks))
                        (constructor
                          NativeTelemetrySinkAction
                          NativeTelemetrySinkIssueSyscall
                          (constructor LinuxSyscallRequest LinuxWrite descriptor bytes))))))))))
        (branch
          LinuxReadSucceeded
          bytes
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSeekSucceeded
          position
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxWriteSucceeded
          written
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxIoctlSucceeded
          output
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxMmapSucceeded
          address
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxUnitSucceeded
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSyscallFailed
          error
          errno
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryOpenFailed)
            state)))))

def nativeTelemetrySinkAfterWrite =
  (lambda unrestricted response : (family LinuxSyscallResponse) .
    (lambda unrestricted state : (family NativeTelemetrySinkState) .
      (eliminate
        LinuxSyscallResponse
        (lambda unrestricted current : (family LinuxSyscallResponse) .
          (family NativeTelemetrySinkDecision))
        response
        (branch
          LinuxOpenSucceeded
          descriptor
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxReadSucceeded
          bytes
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSeekSucceeded
          position
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxWriteSucceeded
          written
          .
          (eliminate
            NativeTelemetrySinkState
            (lambda unrestricted current : (family NativeTelemetrySinkState) .
              (family NativeTelemetrySinkDecision))
            state
            (branch
              NativeTelemetrySinkStateValue
              path
              record
              phase
              optionalDescriptor
              telemetry
              .
              (eliminate
                NativeTelemetryOptionalDescriptor
                (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
                  (family NativeTelemetrySinkDecision))
                optionalDescriptor
                (branch
                  NativeTelemetryNoDescriptor
                  .
                  (constructor
                    NativeTelemetrySinkDecision
                    NativeTelemetrySinkRejected
                    (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
                    state))
                (branch
                  NativeTelemetrySomeDescriptor
                  descriptor
                  .
                  (eliminate
                    NativeTelemetryEncodedRecord
                    (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
                      (family NativeTelemetrySinkDecision))
                    record
                    (branch
                      NativeTelemetryEncodedRecordValue
                      bytes
                      extent
                      digest
                      identity
                      .
                      (nat-eliminate
                        (lambda unrestricted exact : Nat . (family NativeTelemetrySinkDecision))
                        (constructor
                          NativeTelemetrySinkDecision
                          NativeTelemetrySinkRejected
                          (constructor NativeTelemetryErrorCode NativeTelemetryWriteShort)
                          state)
                        (lambda unrestricted exactPredecessor : Nat .
                          (lambda unrestricted ignoredExact : (family NativeTelemetrySinkDecision) .
                            (eliminate
                              NativeTelemetrySinkTelemetry
                              (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
                                (family NativeTelemetrySinkDecision))
                              telemetry
                              (branch
                                NativeTelemetrySinkTelemetryValue
                                planned
                                completed
                                plannedBytes
                                oldWritten
                                syncs
                                closes
                                failures
                                fallbacks
                                .
                                (constructor
                                  NativeTelemetrySinkDecision
                                  NativeTelemetrySinkContinue
                                  (constructor
                                    NativeTelemetrySinkState
                                    NativeTelemetrySinkStateValue
                                    path
                                    record
                                    (constructor
                                      NativeTelemetrySinkPhase
                                      NativeTelemetrySinkSyncing)
                                    optionalDescriptor
                                    (constructor
                                      NativeTelemetrySinkTelemetry
                                      NativeTelemetrySinkTelemetryValue
                                      (succ planned)
                                      (succ completed)
                                      plannedBytes
                                      written
                                      syncs
                                      closes
                                      failures
                                      fallbacks))
                                  (constructor
                                    NativeTelemetrySinkAction
                                    NativeTelemetrySinkIssueSyscall
                                    (constructor LinuxSyscallRequest LinuxFdatasync descriptor)))))))
                        (modelWord64Equal written extent)))))))))
        (branch
          LinuxIoctlSucceeded
          output
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxMmapSucceeded
          address
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxUnitSucceeded
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSyscallFailed
          error
          errno
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryWriteFailed)
            state)))))

def nativeTelemetrySinkAfterSync =
  (lambda unrestricted response : (family LinuxSyscallResponse) .
    (lambda unrestricted state : (family NativeTelemetrySinkState) .
      (eliminate
        LinuxSyscallResponse
        (lambda unrestricted current : (family LinuxSyscallResponse) .
          (family NativeTelemetrySinkDecision))
        response
        (branch
          LinuxOpenSucceeded
          descriptor
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxReadSucceeded
          bytes
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSeekSucceeded
          position
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxWriteSucceeded
          written
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxIoctlSucceeded
          output
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxMmapSucceeded
          address
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxUnitSucceeded
          .
          (eliminate
            NativeTelemetrySinkState
            (lambda unrestricted current : (family NativeTelemetrySinkState) .
              (family NativeTelemetrySinkDecision))
            state
            (branch
              NativeTelemetrySinkStateValue
              path
              record
              phase
              optionalDescriptor
              telemetry
              .
              (eliminate
                NativeTelemetryOptionalDescriptor
                (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
                  (family NativeTelemetrySinkDecision))
                optionalDescriptor
                (branch
                  NativeTelemetryNoDescriptor
                  .
                  (constructor
                    NativeTelemetrySinkDecision
                    NativeTelemetrySinkRejected
                    (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
                    state))
                (branch
                  NativeTelemetrySomeDescriptor
                  descriptor
                  .
                  (eliminate
                    NativeTelemetrySinkTelemetry
                    (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
                      (family NativeTelemetrySinkDecision))
                    telemetry
                    (branch
                      NativeTelemetrySinkTelemetryValue
                      planned
                      completed
                      plannedBytes
                      written
                      syncs
                      closes
                      failures
                      fallbacks
                      .
                      (constructor
                        NativeTelemetrySinkDecision
                        NativeTelemetrySinkContinue
                        (constructor
                          NativeTelemetrySinkState
                          NativeTelemetrySinkStateValue
                          path
                          record
                          (constructor NativeTelemetrySinkPhase NativeTelemetrySinkClosing)
                          optionalDescriptor
                          (constructor
                            NativeTelemetrySinkTelemetry
                            NativeTelemetrySinkTelemetryValue
                            (succ planned)
                            (succ completed)
                            plannedBytes
                            written
                            (succ syncs)
                            closes
                            failures
                            fallbacks))
                        (constructor
                          NativeTelemetrySinkAction
                          NativeTelemetrySinkIssueSyscall
                          (constructor LinuxSyscallRequest LinuxClose descriptor))))))))))
        (branch
          LinuxSyscallFailed
          error
          errno
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetrySyncFailed)
            state)))))

def nativeTelemetrySinkAfterClose =
  (lambda unrestricted response : (family LinuxSyscallResponse) .
    (lambda unrestricted state : (family NativeTelemetrySinkState) .
      (eliminate
        LinuxSyscallResponse
        (lambda unrestricted current : (family LinuxSyscallResponse) .
          (family NativeTelemetrySinkDecision))
        response
        (branch
          LinuxOpenSucceeded
          descriptor
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxReadSucceeded
          bytes
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxSeekSucceeded
          position
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxWriteSucceeded
          written
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxIoctlSucceeded
          output
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxMmapSucceeded
          address
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
            state))
        (branch
          LinuxUnitSucceeded
          .
          (eliminate
            NativeTelemetrySinkState
            (lambda unrestricted current : (family NativeTelemetrySinkState) .
              (family NativeTelemetrySinkDecision))
            state
            (branch
              NativeTelemetrySinkStateValue
              path
              record
              phase
              descriptor
              telemetry
              .
              (eliminate
                NativeTelemetrySinkTelemetry
                (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
                  (family NativeTelemetrySinkDecision))
                telemetry
                (branch
                  NativeTelemetrySinkTelemetryValue
                  planned
                  completed
                  plannedBytes
                  written
                  syncs
                  closes
                  failures
                  fallbacks
                  .
                  (constructor
                    NativeTelemetrySinkDecision
                    NativeTelemetrySinkFinished
                    record
                    (constructor
                      NativeTelemetrySinkTelemetry
                      NativeTelemetrySinkTelemetryValue
                      planned
                      (succ completed)
                      plannedBytes
                      written
                      syncs
                      (succ closes)
                      failures
                      fallbacks)))))))
        (branch
          LinuxSyscallFailed
          error
          errno
          .
          (constructor
            NativeTelemetrySinkDecision
            NativeTelemetrySinkRejected
            (constructor NativeTelemetryErrorCode NativeTelemetryCloseFailed)
            state)))))