A scalar snapshot fits in any admitted larger body bound. The typed drain
can replace the copied scalar payload before sealing; this routine itself
still prepares version-two scalar bytes and never claims typed admission.
134def nativeTelemetryPublicationPrepareRoutineForBody =
135 (lambda unrestricted ordinaryCapacity : Nat .
136 (lambda unrestricted reservedCapacity : Nat .
137 (lambda unrestricted bodyBytes : Nat .
138 (aosChoose
139 Bytes
140 (naturalAnd
141 (naturalLessOrEqual
142 (publicationBodyMaximumBytes ordinaryCapacity reservedCapacity)
143 bodyBytes)
144 (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes))
145 (nativeTelemetryPublicationRoutineFor
146 (constructor
147 TelemetryPublicationRoutineKind
148 TelemetryPublicationPrepareRoutine
149 ordinaryCapacity
150 reservedCapacity
151 bodyBytes))
152 b""))))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.