Runtime.NativeTelemetry

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