127def nativeObservedCaptureAdmission =
128 (lambda unrestricted applicationBytes : Nat .
129 (lambda unrestricted applicationSlots : Nat .
130 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
131 (lambda unrestricted wanted : Nat .
132 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
133 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
134 (eliminate
135 TelemetryRoutedPolicyPlan
136 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . Nat)
137 plan
138 (branch
139 TelemetryRoutedPolicyReady
140 policy
141 sites
142 drain
143 .
144 (eliminate
145 TelemetryDispatchPlan
146 (lambda unrestricted current : (family TelemetryDispatchPlan) . Nat)
147 drain
148 (branch
149 TelemetryDispatchReady
150 oc
151 rc
152 ordinaryRoutes
153 reservedRoutes
154 ordinary
155 reserved
156 descriptors
157 bound
158 .
159 (eliminate
160 TelemetryPolicySites
161 (lambda unrestricted current : (family TelemetryPolicySites) . Nat)
162 (telemetryPolicySiteLookup wanted sites)
163 (branch TelemetryPolicySitesEnd . 0)
164 (branch
165 TelemetryPolicySitesNext
166 tag
167 site
168 declaration
169 following
170 induction
171 .
172 (aosChoose
173 Nat
174 (captureSiteSelected policy site)
175 (naturalAnd
176 (naturalAnd
177 (nativeTelemetrySourcesAdmission
178 (telemetryRecordRouteLookup
179 tag
180 (aosChoose
181 (family TelemetryRecordRoutes)
182 (captureSiteReserved site)
183 reservedRoutes
184 ordinaryRoutes))
185 values)
186 (nativeTelemetrySourceScopesWith
187 (telemetryRecordRouteLookup
188 tag
189 (aosChoose
190 (family TelemetryRecordRoutes)
191 (captureSiteReserved site)
192 reservedRoutes
193 ordinaryRoutes))
194 values
195 (nativePhysicalOperandScopeAdmission
196 applicationBytes
197 applicationSlots
198 0)))
199 (naturalOr
200 (naturalEqual (captureSiteStride site) 1)
201 (nativePhysicalOperandScopeAdmission
202 applicationBytes
203 applicationSlots
204 0
205 coordinate)))
206 1))))
207 (branch TelemetryDispatchRefused reason . 0)))
208 (branch TelemetryRoutedPolicyRefused reason . 0))))))))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.