334def publicationStorageCertificateForBody =
335 (lambda unrestricted applicationBytes : Nat .
336 (lambda unrestricted ordinaryCapacity : Nat .
337 (lambda unrestricted reservedCapacity : Nat .
338 (lambda unrestricted bodyBytes : Nat .
339 (naturalAnd
340 (naturalAnd
341 (naturalEqual telemetryIdentitySetBytes nativeTelemetryDigestBytes)
342 (naturalLessOrEqual publicationPayloadRecordsAt bodyBytes))
343 (naturalAnd
344 (captureWithIdentityArenaCertificate
345 applicationBytes
346 ordinaryCapacity
347 reservedCapacity)
348 (naturalAnd
349 (naturalLessOrEqual (publicationRecordBytes bodyBytes) publicationMaximumFrameBytes)
350 (naturalAnd
351 (naturalLessOrEqual
352 (publicationWholeArenaBytesForBody
353 applicationBytes
354 ordinaryCapacity
355 reservedCapacity
356 bodyBytes)
357 captureExtentMaximum)
358 (arenaCertificate
359 (publicationWholeArenaBytesForBody
360 applicationBytes
361 ordinaryCapacity
362 reservedCapacity
363 bodyBytes)
364 (publicationWholeArenaResidentsForBody
365 applicationBytes
366 ordinaryCapacity
367 reservedCapacity
368 bodyBytes))))))))))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.