One capture at a declared safe boundary. No caller operation can intervene
between pending acquisition, durable drain and retry of the frozen values.
Retry is bounded once; zero capacity or refusal fails by name. Optional
accounted drops may continue; an inaccessible/poisoned sink may not silently
run unobserved. This is not a concurrent writer or an asynchronous uploader.
1942def nativeTelemetryRoutedCaptureAndContinueCommands =
1943 (lambda unrestricted applicationBytes : Nat .
1944 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
1945 (lambda unrestricted wanted : Nat .
1946 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
1947 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
1948 (lambda unrestricted sink : (family NativePhysicalOperand) .
1949 (lambda unrestricted directory : (family NativePhysicalOperand) .
1950 (lambda unrestricted captureSlot : Nat .
1951 (lambda unrestricted publicationSlot : Nat .
1952 (lambda unrestricted workSlot : Nat .
1953 (lambda unrestricted retrySlot : Nat .
1954 (lambda unrestricted identity : Bytes .
1955 (lambda unrestricted tail : (family NativePhysicalCommands) .
1956 (eliminate
1957 TelemetryRoutedPolicyPlan
1958 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) .
1959 (family NativePhysicalCommands))
1960 plan
1961 (branch
1962 TelemetryRoutedPolicyReady
1963 policy
1964 sites
1965 drain
1966 .
1967 (eliminate
1968 TelemetryPolicySites
1969 (lambda unrestricted current : (family TelemetryPolicySites) .
1970 (family NativePhysicalCommands))
1971 (telemetryPolicySiteLookup wanted sites)
1972 (branch
1973 TelemetryPolicySitesEnd
1974 .
1975 (nativeLaunchRecipeCommand
1976 (constructor
1977 NativePhysicalOperation
1978 NativePhysicalMachineRoutine
1979 b""
1980 (constructor
1981 NativePhysicalArguments
1982 NativePhysicalArgumentsValue
1983 (nativeLaunchRecipeImmediate 0)
1984 (nativeLaunchRecipeImmediate 0)
1985 (nativeLaunchRecipeImmediate 0)
1986 (nativeLaunchRecipeImmediate 0)
1987 (nativeLaunchRecipeImmediate 0)
1988 (nativeLaunchRecipeImmediate 0))
1989 (nativeLaunchRecipeStore captureSlot))
1990 identity
1991 tail))
1992 (branch
1993 TelemetryPolicySitesNext
1994 tag
1995 site
1996 declaration
1997 following
1998 induction
1999 .
2000 (aosChoose
2001 (family NativePhysicalCommands)
2002 (naturalAnd
2003 (naturalIsZero (naturalEqual workSlot retrySlot))
2004 (naturalAnd
2005 (naturalIsZero (naturalEqual publicationSlot retrySlot))
2006 (naturalAnd
2007 (naturalIsZero (naturalEqual publicationSlot workSlot))
2008 (naturalAnd
2009 (naturalIsZero (naturalEqual captureSlot retrySlot))
2010 (naturalAnd
2011 (naturalIsZero (naturalEqual captureSlot workSlot))
2012 (naturalAnd
2013 (naturalIsZero (naturalEqual captureSlot publicationSlot))
2014 1))))))
2015 (nativeTelemetryRoutedCaptureSiteCommand
2016 applicationBytes
2017 plan
2018 wanted
2019 values
2020 coordinate
2021 captureSlot
2022 workSlot
2023 identity
2024 (aosChoose
2025 (family NativePhysicalCommands)
2026 (captureSiteSelected policy site)
2027 (nativeLaunchRecipeCommand
2028 (constructor
2029 NativePhysicalOperation
2030 NativePhysicalMachineRoutine
2031 nativeTelemetryPendingRoutine
2032 (constructor
2033 NativePhysicalArguments
2034 NativePhysicalArgumentsValue
2035 (nativeLaunchRecipeSlotValue captureSlot)
2036 (nativeLaunchRecipeImmediate 0)
2037 (nativeLaunchRecipeImmediate 0)
2038 (nativeLaunchRecipeImmediate 0)
2039 (nativeLaunchRecipeImmediate 0)
2040 (nativeLaunchRecipeImmediate 0))
2041 (nativeLaunchRecipeStore retrySlot))
2042 identity
2043 (nativeLaunchRecipeCommand
2044 (constructor
2045 NativePhysicalOperation
2046 NativePhysicalRepeatBeginCounted
2047 (nativeLaunchRecipeSlotValue retrySlot))
2048 identity
2049 (nativeTelemetryRoutedPolicyBoundaryCommands
2050 applicationBytes
2051 plan
2052 0
2053 sink
2054 directory
2055 captureSlot
2056 publicationSlot
2057 workSlot
2058 identity
2059 (nativeLaunchRecipeAssertEqual
2060 (nativeLaunchRecipeSlotValue publicationSlot)
2061 (nativeLaunchRecipeImmediate 0)
2062 (nativeTelemetryFailureIdentity
2063 b"telemetry:pending-drain-refused")
2064 (nativeTelemetryDispatchCaptureCommand
2065 applicationBytes
2066 drain
2067 1
2068 (captureSiteReserved site)
2069 wanted
2070 captureSlot
2071 identity
2072 (nativeLaunchRecipeAssertEqual
2073 (nativeLaunchRecipeSlotValue captureSlot)
2074 (nativeLaunchRecipeImmediate 1)
2075 (nativeTelemetryFailureIdentity
2076 b"telemetry:pending-retry-refused")
2077 (nativeLaunchRecipeCommand
2078 (constructor
2079 NativePhysicalOperation
2080 NativePhysicalRepeatEnd)
2081 identity
2082 (nativeLaunchRecipeCommand
2083 (constructor
2084 NativePhysicalOperation
2085 NativePhysicalMachineRoutine
2086 (nativeTelemetryContinuationRoutine
2087 (capturePolicyRequired policy))
2088 (constructor
2089 NativePhysicalArguments
2090 NativePhysicalArgumentsValue
2091 (nativeLaunchRecipeSlotValue captureSlot)
2092 (nativeLaunchRecipeImmediate 0)
2093 (nativeLaunchRecipeImmediate 0)
2094 (nativeLaunchRecipeImmediate 0)
2095 (nativeLaunchRecipeImmediate 0)
2096 (nativeLaunchRecipeImmediate 0))
2097 (nativeLaunchRecipeStore retrySlot))
2098 identity
2099 (nativeLaunchRecipeAssertEqual
2100 (nativeLaunchRecipeSlotValue retrySlot)
2101 (nativeLaunchRecipeImmediate 1)
2102 (nativeTelemetryFailureIdentity
2103 b"telemetry:capture-refused")
2104 (nativeTelemetryRoutedPolicyBoundaryCommands
2105 applicationBytes
2106 plan
2107 0
2108 sink
2109 directory
2110 captureSlot
2111 publicationSlot
2112 workSlot
2113 identity
2114 (nativeLaunchRecipeCommand
2115 (constructor
2116 NativePhysicalOperation
2117 NativePhysicalAssertOneOf
2118 (nativeLaunchRecipeSlotValue publicationSlot)
2119 (nativeLaunchRecipeImmediate 0)
2120 (nativeLaunchRecipeImmediate 7)
2121 (constructor
2122 NativePhysicalErrorCode
2123 NativePhysicalExecutionAssertionFailed))
2124 (nativeTelemetryFailureIdentity
2125 b"telemetry:publication-refused")
2126 tail)))))))))))
2127 (nativeLaunchRecipeCommand
2128 (constructor
2129 NativePhysicalOperation
2130 NativePhysicalMachineRoutine
2131 (nativeTelemetryContinuationRoutine
2132 (capturePolicyRequired policy))
2133 (constructor
2134 NativePhysicalArguments
2135 NativePhysicalArgumentsValue
2136 (nativeLaunchRecipeSlotValue captureSlot)
2137 (nativeLaunchRecipeImmediate 0)
2138 (nativeLaunchRecipeImmediate 0)
2139 (nativeLaunchRecipeImmediate 0)
2140 (nativeLaunchRecipeImmediate 0)
2141 (nativeLaunchRecipeImmediate 0))
2142 (nativeLaunchRecipeStore retrySlot))
2143 identity
2144 (nativeLaunchRecipeAssertEqual
2145 (nativeLaunchRecipeSlotValue retrySlot)
2146 (nativeLaunchRecipeImmediate 1)
2147 (nativeTelemetryFailureIdentity
2148 b"telemetry:capture-refused")
2149 (nativeTelemetryRoutedPolicyBoundaryCommands
2150 applicationBytes
2151 plan
2152 0
2153 sink
2154 directory
2155 captureSlot
2156 publicationSlot
2157 workSlot
2158 identity
2159 (nativeLaunchRecipeCommand
2160 (constructor
2161 NativePhysicalOperation
2162 NativePhysicalAssertOneOf
2163 (nativeLaunchRecipeSlotValue publicationSlot)
2164 (nativeLaunchRecipeImmediate 0)
2165 (nativeLaunchRecipeImmediate 7)
2166 (constructor
2167 NativePhysicalErrorCode
2168 NativePhysicalExecutionAssertionFailed))
2169 (nativeTelemetryFailureIdentity
2170 b"telemetry:publication-refused")
2171 tail))))))
2172 (nativeLaunchRecipeCommand
2173 (constructor
2174 NativePhysicalOperation
2175 NativePhysicalMachineRoutine
2176 b""
2177 (constructor
2178 NativePhysicalArguments
2179 NativePhysicalArgumentsValue
2180 (nativeLaunchRecipeImmediate 0)
2181 (nativeLaunchRecipeImmediate 0)
2182 (nativeLaunchRecipeImmediate 0)
2183 (nativeLaunchRecipeImmediate 0)
2184 (nativeLaunchRecipeImmediate 0)
2185 (nativeLaunchRecipeImmediate 0))
2186 (nativeLaunchRecipeStore captureSlot))
2187 identity
2188 tail)))))
2189 (branch
2190 TelemetryRoutedPolicyRefused
2191 reason
2192 .
2193 (nativeLaunchRecipeCommand
2194 (constructor
2195 NativePhysicalOperation
2196 NativePhysicalMachineRoutine
2197 b""
2198 (constructor
2199 NativePhysicalArguments
2200 NativePhysicalArgumentsValue
2201 (nativeLaunchRecipeImmediate 0)
2202 (nativeLaunchRecipeImmediate 0)
2203 (nativeLaunchRecipeImmediate 0)
2204 (nativeLaunchRecipeImmediate 0)
2205 (nativeLaunchRecipeImmediate 0)
2206 (nativeLaunchRecipeImmediate 0))
2207 (nativeLaunchRecipeStore captureSlot))
2208 identity
2209 tail))))))))))))))))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.