799def nativeTelemetrySinkAfterWrite =
800 (lambda unrestricted response : (family LinuxSyscallResponse) .
801 (lambda unrestricted state : (family NativeTelemetrySinkState) .
802 (eliminate
803 LinuxSyscallResponse
804 (lambda unrestricted current : (family LinuxSyscallResponse) .
805 (family NativeTelemetrySinkDecision))
806 response
807 (branch
808 LinuxOpenSucceeded
809 descriptor
810 .
811 (constructor
812 NativeTelemetrySinkDecision
813 NativeTelemetrySinkRejected
814 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
815 state))
816 (branch
817 LinuxReadSucceeded
818 bytes
819 .
820 (constructor
821 NativeTelemetrySinkDecision
822 NativeTelemetrySinkRejected
823 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
824 state))
825 (branch
826 LinuxSeekSucceeded
827 position
828 .
829 (constructor
830 NativeTelemetrySinkDecision
831 NativeTelemetrySinkRejected
832 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
833 state))
834 (branch
835 LinuxWriteSucceeded
836 written
837 .
838 (eliminate
839 NativeTelemetrySinkState
840 (lambda unrestricted current : (family NativeTelemetrySinkState) .
841 (family NativeTelemetrySinkDecision))
842 state
843 (branch
844 NativeTelemetrySinkStateValue
845 path
846 record
847 phase
848 optionalDescriptor
849 telemetry
850 .
851 (eliminate
852 NativeTelemetryOptionalDescriptor
853 (lambda unrestricted current : (family NativeTelemetryOptionalDescriptor) .
854 (family NativeTelemetrySinkDecision))
855 optionalDescriptor
856 (branch
857 NativeTelemetryNoDescriptor
858 .
859 (constructor
860 NativeTelemetrySinkDecision
861 NativeTelemetrySinkRejected
862 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
863 state))
864 (branch
865 NativeTelemetrySomeDescriptor
866 descriptor
867 .
868 (eliminate
869 NativeTelemetryEncodedRecord
870 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
871 (family NativeTelemetrySinkDecision))
872 record
873 (branch
874 NativeTelemetryEncodedRecordValue
875 bytes
876 extent
877 digest
878 identity
879 .
880 (nat-eliminate
881 (lambda unrestricted exact : Nat . (family NativeTelemetrySinkDecision))
882 (constructor
883 NativeTelemetrySinkDecision
884 NativeTelemetrySinkRejected
885 (constructor NativeTelemetryErrorCode NativeTelemetryWriteShort)
886 state)
887 (lambda unrestricted exactPredecessor : Nat .
888 (lambda unrestricted ignoredExact : (family NativeTelemetrySinkDecision) .
889 (eliminate
890 NativeTelemetrySinkTelemetry
891 (lambda unrestricted current : (family NativeTelemetrySinkTelemetry) .
892 (family NativeTelemetrySinkDecision))
893 telemetry
894 (branch
895 NativeTelemetrySinkTelemetryValue
896 planned
897 completed
898 plannedBytes
899 oldWritten
900 syncs
901 closes
902 failures
903 fallbacks
904 .
905 (constructor
906 NativeTelemetrySinkDecision
907 NativeTelemetrySinkContinue
908 (constructor
909 NativeTelemetrySinkState
910 NativeTelemetrySinkStateValue
911 path
912 record
913 (constructor
914 NativeTelemetrySinkPhase
915 NativeTelemetrySinkSyncing)
916 optionalDescriptor
917 (constructor
918 NativeTelemetrySinkTelemetry
919 NativeTelemetrySinkTelemetryValue
920 (succ planned)
921 (succ completed)
922 plannedBytes
923 written
924 syncs
925 closes
926 failures
927 fallbacks))
928 (constructor
929 NativeTelemetrySinkAction
930 NativeTelemetrySinkIssueSyscall
931 (constructor LinuxSyscallRequest LinuxFdatasync descriptor)))))))
932 (modelWord64Equal written extent)))))))))
933 (branch
934 LinuxIoctlSucceeded
935 output
936 .
937 (constructor
938 NativeTelemetrySinkDecision
939 NativeTelemetrySinkRejected
940 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
941 state))
942 (branch
943 LinuxMmapSucceeded
944 address
945 .
946 (constructor
947 NativeTelemetrySinkDecision
948 NativeTelemetrySinkRejected
949 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
950 state))
951 (branch
952 LinuxUnitSucceeded
953 .
954 (constructor
955 NativeTelemetrySinkDecision
956 NativeTelemetrySinkRejected
957 (constructor NativeTelemetryErrorCode NativeTelemetryUnexpectedResponse)
958 state))
959 (branch
960 LinuxSyscallFailed
961 error
962 errno
963 .
964 (constructor
965 NativeTelemetrySinkDecision
966 NativeTelemetrySinkRejected
967 (constructor NativeTelemetryErrorCode NativeTelemetryWriteFailed)
968 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.