Append preflight's byte contract; the native realization additionally checks
the rendered status and readiness before touching staged event bytes.
429def telemetryDrainAppendAdmission =
430 (lambda unrestricted ready : Nat .
431 (lambda unrestricted status : Nat .
432 (lambda unrestricted bodyBytes : Nat .
433 (lambda unrestricted recordBytes : Nat .
434 (lambda unrestricted bound : Nat .
435 (lambda unrestricted publicationExtent : Nat .
436 (lambda unrestricted recordExtent : Nat .
437 (naturalAnd
438 (naturalEqual publicationExtent (publicationArenaBytesForBody bound))
439 (naturalAnd
440 (naturalLessOrEqual recordBytes bound)
441 (naturalAnd
442 (naturalLessOrEqual (naturalAdd telemetryRecordAt recordBytes) recordExtent)
443 (naturalAnd
444 (naturalEqual ready 1)
445 (naturalAnd
446 (naturalEqual status 0)
447 (naturalAnd
448 (naturalLessOrEqual publicationPayloadRecordsAt bodyBytes)
449 (naturalLessOrEqual (naturalAdd bodyBytes (succ recordBytes)) 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.