Bounds are derived from the declared capacities/recipes, while actual byte
lengths follow occupancy. An empty queue emits no event. Render refusal
leaves all captures pending; a durable commit alone reclaims the queues.
358def drainPreparedWith =
359 (lambda unrestricted applicationBytes : Nat .
360 (lambda unrestricted ordinaryCapacity : Nat .
361 (lambda unrestricted reservedCapacity : Nat .
362 (lambda unrestricted ordinaryDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
363 (lambda unrestricted reservedDrain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
364 (lambda unrestricted descriptors : Bytes .
365 (lambda unrestricted bound : Nat .
366 (lambda unrestricted terminal : Nat .
367 (lambda unrestricted sink : (family NativePhysicalOperand) .
368 (lambda unrestricted directory : (family NativePhysicalOperand) .
369 (lambda unrestricted resultSlot : Nat .
370 (lambda unrestricted identity : Bytes .
371 (lambda unrestricted tail : (family NativePhysicalCommands) .
372 (nativeTelemetryPublicationPrepareCommandsForBody
373 applicationBytes
374 ordinaryCapacity
375 reservedCapacity
376 bound
377 terminal
378 resultSlot
379 identity
380 (nativeLaunchRecipeCommand
381 (constructor
382 NativePhysicalOperation
383 NativePhysicalRepeatBeginCounted
384 (publicationStateLoad
385 applicationBytes
386 ordinaryCapacity
387 reservedCapacity
388 publicationReadyAt))
389 identity
390 (publicationCopyPayload
391 applicationBytes
392 ordinaryCapacity
393 reservedCapacity
394 (naturalAdd publicationBodyAt publicationPayloadRecordsAt)
395 descriptors
396 identity
397 (drainStore
398 (naturalAdd
399 (publicationBase
400 applicationBytes
401 ordinaryCapacity
402 reservedCapacity)
403 publicationBodyLengthAt)
404 (nativeLaunchRecipeImmediate
405 (naturalAdd
406 publicationPayloadRecordsAt
407 (bytes-length descriptors)))
408 identity
409 (drainStore
410 (naturalAdd
411 (publicationBase
412 applicationBytes
413 ordinaryCapacity
414 reservedCapacity)
415 (naturalAdd
416 publicationBodyAt
417 nativeTelemetryEmptyErrorPayloadExtentAt))
418 (nativeLaunchRecipeImmediate
419 (naturalAdd captureWordBytes (bytes-length descriptors)))
420 identity
421 (ordinaryDrain
422 (reservedDrain
423 (nativeLaunchRecipeCommand
424 (constructor
425 NativePhysicalOperation
426 NativePhysicalMachineRoutine
427 (nativeTelemetryPublicationTypedPaddingRoutineForBody bound)
428 (constructor
429 NativePhysicalArguments
430 NativePhysicalArgumentsValue
431 (publicationStateAddress
432 applicationBytes
433 ordinaryCapacity
434 reservedCapacity
435 0)
436 (nativeLaunchRecipeImmediate
437 (publicationArenaBytesForBody bound))
438 (publicationStateLoad
439 applicationBytes
440 ordinaryCapacity
441 reservedCapacity
442 (naturalAdd
443 publicationBodyAt
444 nativeTelemetryEmptyErrorPayloadExtentAt))
445 (nativeLaunchRecipeImmediate 0)
446 (nativeLaunchRecipeImmediate 0)
447 (nativeLaunchRecipeImmediate 0))
448 (nativeLaunchRecipeStore resultSlot))
449 identity
450 (nativeLaunchRecipeCommand
451 (constructor
452 NativePhysicalOperation
453 NativePhysicalRepeatEnd)
454 identity
455 (publicationSealAndCommitCommandsForBody
456 applicationBytes
457 ordinaryCapacity
458 reservedCapacity
459 bound
460 sink
461 directory
462 resultSlot
463 identity
464 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.