Check source scopes before extending storage. Finish closes observation,
not application success: cleanup may follow, but capture cannot. Closing
inside a repeat would invalidate later iterations and is refused statically.
246def nativeObservedStepsAdmission =
247 (lambda unrestricted applicationBytes : Nat .
248 (lambda unrestricted applicationSlots : Nat .
249 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
250 (lambda unrestricted steps : (family NativeObservedSteps) .
251 (app
252 (eliminate
253 NativeObservedSteps
254 (lambda unrestricted current : (family NativeObservedSteps) .
255 (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)))
256 steps
257 (branch
258 NativeObservedStepsEnd
259 .
260 (lambda unrestricted depth : Nat .
261 (lambda unrestricted closed : Nat . (naturalIsZero depth))))
262 (branch
263 NativeObservedOperation
264 operation
265 following
266 induction
267 .
268 (nativeObservedAdmitOperation applicationBytes applicationSlots operation induction))
269 (branch
270 NativeObservedCommand
271 command
272 following
273 induction
274 .
275 (eliminate
276 NativePhysicalCommand
277 (lambda unrestricted current : (family NativePhysicalCommand) .
278 (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)))
279 command
280 (branch
281 NativePhysicalCommandValue
282 operation
283 errorIdentity
284 .
285 (nativeObservedAdmitOperation
286 applicationBytes
287 applicationSlots
288 operation
289 induction))))
290 (branch
291 NativeObservedOpenJournal
292 pathAt
293 fileSlot
294 directorySlot
295 following
296 induction
297 .
298 (lambda unrestricted depth : Nat .
299 (lambda unrestricted closed : Nat .
300 (naturalAnd
301 (naturalIsZero depth)
302 (naturalAnd
303 (naturalIsZero closed)
304 (naturalAnd
305 (nativeObservedJournalAdmission
306 applicationBytes
307 applicationSlots
308 pathAt
309 fileSlot
310 directorySlot)
311 (induction depth closed)))))))
312 (branch
313 NativeObservedCaptureBoundary
314 tag
315 values
316 coordinate
317 following
318 induction
319 .
320 (lambda unrestricted depth : Nat .
321 (lambda unrestricted closed : Nat .
322 (naturalAnd
323 (naturalIsZero closed)
324 (naturalAnd
325 (nativeObservedCaptureAdmission
326 applicationBytes
327 applicationSlots
328 plan
329 tag
330 values
331 coordinate)
332 (induction depth closed))))))
333 (branch
334 NativeObservedFinish
335 following
336 induction
337 .
338 (lambda unrestricted depth : Nat .
339 (lambda unrestricted closed : Nat .
340 (naturalAnd
341 (naturalIsZero depth)
342 (naturalAnd (naturalIsZero closed) (induction depth 1)))))))
343 0
344 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.