ABI: publication arena, rendered-record arena, event bytes, exact publication
extent, record extent. The caller's arena certificate supplies live disjoint
buffers. Invalid publication extent refuses without touching its pointer;
once accessible, any rejection clears readiness before a later seal.
Success records the bounded destination and LF and advances the private byte
cursor. The maintained memory-copy owner then copies the event bytes before
the next iteration; no external reader can see this unsealed staging area.
110def drainAppendAssembly =
111 (lambda unrestricted bound : Nat .
112 (telemetryDrainAssemblyFor
113 (family X86NativeAssembly)
114 (family X86NativeRegister64)
115 drainX86Backend
116 (constructor TelemetryDrainRoutineKind TelemetryDrainAppendRoutine bound)))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.